Theory OpSem_Deadlock_Results

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : Deadlock Results
 *
 * 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.
 ******************************************************************************›
(*>*)

section‹ Deadlock Results ›

(*<*)
theory  OpSem_Deadlock_Results
  imports After_Trace_Operator
begin
(*>*)


lemma initial_ev_imp_in_events_of: ‹ev a ∈ P0 ⟹ a ∈ α(P)›
  by (meson AfterExt.events_of_iff_reachable_ev AfterExt.initial_ev_reachable)

lemma initial_tick_imp_in_ticks_of: ‹✓(r) ∈ P0 ⟹ r ∈ ✓s(P)›
  by (meson AfterExt.initial_tick_reachable AfterExt.ticks_of_iff_reachable_tick)

lemma ‹UNIV ∈ ℛ P ⟷ P ⊑F STOP›
  unfolding failure_refine_def
  apply (simp add: D_STOP F_STOP Refusals_iff)
  using is_processT4 by blast

lemma no_events_of_if_at_most_initial_tick: ‹P0 ⊆ range tick ⟹ α(P) = {}›
  using empty_ev_initials_iff_empty_events_of by fast

lemma deadlock_free_initial_evE:
  ‹deadlock_free P ⟹ (⋀a. ev a ∈ P0 ⟹ thesis) ⟹ thesis›
  using empty_ev_initials_iff_empty_events_of
        nonempty_events_of_if_deadlock_free by fastforce


context AfterExt
begin

text ‹As we said earlier, @{const [source] Aftertrace} allows us to obtain some 
      very powerful results about const‹deadlock_free› and const‹deadlock_freeSKIPS›.›

subsection ‹Preliminaries and induction Rules›

context fixes P :: ‹('a, 'r) processptick› begin

lemma initials_Aftertrace_subset_events_of:
  ‹(P after𝒯 t)0 ⊆ ev ` α(P)› if ‹non_terminating P› ‹t ∈ 𝒯 P›
proof -
  have ‹tF t ⟹ ev a ∈ (P after𝒯 t)0 ⟹ reachable_ev P a› for a
    using reachable_ev_iff_in_initials_Aftertrace_for_some_tickFree_T that(2) by blast
  also have ‹tF t ∧ range tick ∩ (P after𝒯 t)0 = {}›
    by (simp add: disjoint_iff image_iff)
       (metis T_Aftertrace_eq initials_def mem_Collect_eq non_terminating_is_right
              non_tickFree_tick that(1) that(2) tickFree_append_iff)
  ultimately show ‹(P after𝒯 t)0 ⊆ ev ` α(P)›
    by (simp add: subset_iff image_iff disjoint_iff)
       (metis eventptick.exhaust events_of_iff_reachable_ev)
qed

end



text ‹With the next result, the general idea appears: instead of doing an induction only
      on the process term‹P› we are interested in, we include a quantification over all
      the processes than can be reached from term‹P› after some trace of term‹P›.›

theorem Aftertrace_fix_ind [consumes 2, case_names cont step]:
    fixes ref :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infix ‹⊑ref› 60)
  assumes adm_ref : ‹⋀u v. cont (u :: ('a, 'r) processptick ⇒ ('a, 'r) processptick) ⟹ monofun v
                            ⟹ adm (λx. u x ⊑ref v x)›
      and BOT_le_ref : ‹⋀Q. ⊥ ⊑ref Q›
      and cont_f : ‹cont f›
      and hyp : ‹⋀s x. ∀Q ∈ {Q. ∃s ∈ 𝒯 P. g s Q ∧ Q = P after𝒯 s}. x ⊑ref Q ⟹
                       s ∈ 𝒯 P ⟹ g s (P after𝒯 s) ⟹ f x ⊑ref P after𝒯 s›
  shows ‹∀Q ∈ {Q. ∃s ∈ 𝒯 P. g s Q ∧ Q = P after𝒯 s}. (μ X. f X) ⊑ref Q›
  apply (induct rule: fix_ind)
    apply (solves ‹simp add: adm_ref monofunI›)
   apply (solves ‹simp add: BOT_le_ref›)
  using hyp cont_f by auto


lemma Aftertrace_fix_ind_F [consumes 1, case_names cont step]:
  ‹⟦Q ∈ {Q. ∃t ∈ 𝒯 P. g t Q ∧ Q = P after𝒯 t}; cont f;
    ⋀t x. ⟦∀Q ∈ {Q. ∃t ∈ 𝒯 P. g t Q ∧ Q = P after𝒯 t}. x ⊑F Q;
           t ∈ 𝒯 P; g t (P after𝒯 t)⟧ ⟹ f x ⊑F P after𝒯 t⟧ ⟹
    (μ X. f X) ⊑F Q›
  and Aftertrace_fix_ind_D [consumes 1, case_names cont step]:
  ‹⟦Q ∈ {Q. ∃t ∈ 𝒯 P. g t Q ∧ Q = P after𝒯 t}; cont f;
    ⋀t x. ⟦∀Q ∈ {Q. ∃t ∈ 𝒯 P. g t Q ∧ Q = P after𝒯 t}. x ⊑D Q;
           t ∈ 𝒯 P; g t (P after𝒯 t)⟧ ⟹ f x ⊑D P after𝒯 t⟧ ⟹
    (μ X. f X) ⊑D Q›
  and Aftertrace_fix_ind_T [consumes 1, case_names cont step]:
  ‹⟦Q ∈ {Q. ∃t ∈ 𝒯 P. g t Q ∧ Q = P after𝒯 t}; cont f;
    ⋀t x. ⟦∀Q ∈ {Q. ∃t ∈ 𝒯 P. g t Q ∧ Q = P after𝒯 t}. x ⊑T Q;
           t ∈ 𝒯 P; g t (P after𝒯 t)⟧ ⟹ f x ⊑T P after𝒯 t⟧ ⟹
    (μ X. f X) ⊑T Q›
  and Aftertrace_fix_ind_FD [consumes 1, case_names cont step]:
  ‹⟦Q ∈ {Q. ∃t ∈ 𝒯 P. g t Q ∧ Q = P after𝒯 t}; cont f;
    ⋀t x. ⟦∀Q ∈ {Q. ∃t ∈ 𝒯 P. g t Q ∧ Q = P after𝒯 t}. x ⊑FD Q;
           t ∈ 𝒯 P; g t (P after𝒯 t)⟧ ⟹ f x ⊑FD P after𝒯 t⟧ ⟹
    (μ X. f X) ⊑FD Q›
  and Aftertrace_fix_ind_DT [consumes 1, case_names cont step]:
  ‹⟦Q ∈ {Q. ∃t ∈ 𝒯 P. g t Q ∧ Q = P after𝒯 t}; cont f;
    ⋀t x. ⟦∀Q ∈ {Q. ∃t ∈ 𝒯 P. g t Q ∧ Q = P after𝒯 t}. x ⊑DT Q;
           t ∈ 𝒯 P; g t (P after𝒯 t)⟧ ⟹ f x ⊑DT P after𝒯 t⟧ ⟹
    (μ X. f X) ⊑DT Q›
  by (all ‹rule Aftertrace_fix_ind[rule_format]›) simp_all


corollary reachable_processes_fix_ind [consumes 3, case_names cont step]: 
  ‹⟦Q ∈ ℛproc P; 
    ⋀u v. ⟦cont (u :: ('a, 'r) processptick ⇒ ('a, 'r) processptick); monofun v⟧ ⟹ adm (λx. ref (u x) (v x));
    ⋀Q. ref ⊥ Q;
    cont f;
    ⋀t x. ⟦∀Q ∈ ℛproc P. ref x Q; t ∈ 𝒯 P; tickFree t⟧ ⟹ ref (f x) (P after𝒯 t)⟧ ⟹
    ref (μ x. f x) Q›
  by (simp add: reachable_processes_is,
      rule Aftertrace_fix_ind[where g = ‹λs Q. tickFree s›, simplified, rule_format]; simp)

corollary reachable_processes_fix_ind_F [consumes 1, case_names cont step]:
  ‹⟦Q ∈ ℛproc P; cont f; 
    ⋀t x. ∀Q ∈ ℛproc P. x ⊑F Q ⟹ t ∈ 𝒯 P ⟹ tickFree t ⟹ f x ⊑F P after𝒯 t⟧ ⟹
    (μ X. f X) ⊑F Q›
  and reachable_processes_fix_ind_D [consumes 1, case_names cont step]:
  ‹⟦Q ∈ ℛproc P; cont f; 
    ⋀t x. ∀Q ∈ ℛproc P. x ⊑D Q ⟹ t ∈ 𝒯 P ⟹ tickFree t ⟹ f x ⊑D P after𝒯 t⟧ ⟹
    (μ X. f X) ⊑D Q›
  and reachable_processes_fix_ind_T [consumes 1, case_names cont step]:
  ‹⟦Q ∈ ℛproc P; cont f; 
    ⋀t x. ∀Q ∈ ℛproc P. x ⊑T Q ⟹ t ∈ 𝒯 P ⟹ tickFree t ⟹ f x ⊑T P after𝒯 t⟧ ⟹
    (μ X. f X) ⊑T Q›
  and reachable_processes_fix_ind_FD [consumes 1, case_names cont step]:
  ‹⟦Q ∈ ℛproc P; cont f; 
    ⋀t x. ∀Q ∈ ℛproc P. x ⊑FD Q ⟹ t ∈ 𝒯 P ⟹ tickFree t ⟹ f x ⊑FD P after𝒯 t⟧ ⟹
    (μ X. f X) ⊑FD Q›
  and reachable_processes_fix_ind_DT [consumes 1, case_names cont step]:
  ‹⟦Q ∈ ℛproc P; cont f; 
    ⋀t x. ∀Q ∈ ℛproc P. x ⊑DT Q ⟹ t ∈ 𝒯 P ⟹ tickFree t ⟹ f x ⊑DT P after𝒯 t⟧ ⟹
    (μ X. f X) ⊑DT Q›
  by (all ‹rule reachable_processes_fix_ind›) simp_all



subsection ‹New idea: const‹After› induct instead of const‹Aftertrace››

―‹TODO: find something›



subsection ‹New results on term‹ℛproc››

lemma reachable_processes_FD_refinement_propagation_induct [consumes 1, case_names cont base step]:
  ―‹May be generalized or duplicated to other refinements.›
  assumes reachable : ‹(Q :: ('a, 'r) processptick) ∈ ℛproc P›
      and cont_f : ‹cont f›
      and base : ‹(μ x. f x) ⊑FD P›
      and step : ‹⋀a. a ∈ α(P) ⟹ f (μ x. f x) after a = (μ x. f x)›
    shows ‹(μ x. f x) ⊑FD Q›
proof (use reachable in ‹induct rule: reachable_processes.induct›)
  case reachable_self
  show ‹(μ x. f x) ⊑FD P› by (fact base)
next
  case (reachable_after Q a)
  from reachable_after.hyps(2) have ‹f (μ x. f x) ⊑FD Q›
    by (subst (asm) cont_process_rec[OF refl cont_f])
  hence  * : ‹f (μ x. f x) after a ⊑FD Q after a›
    by (simp add: mono_After_FD reachable_after.hyps(3))
  from reachable_after.hyps(1, 3) have ‹a ∈ α(P)›
    using events_of_reachable_processes_subset initial_ev_imp_in_events_of by (metis in_mono)
  hence ** : ‹f (μ x. f x) after a = (μ x. f x)› by (fact local.step)
  from "*"[unfolded "**"] show ‹(μ x. f x) ⊑FD Q after a› .
qed


theorem ℛproc_fix_ind [consumes 3, case_names cont step]:
    fixes ref :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infix ‹⊑ref› 60)
  assumes reachable : ‹Q ∈ ℛproc P›
      and adm_ref : ‹⋀u v. cont (u :: ('a, 'r) processptick ⇒ ('a, 'r) processptick) ⟹ monofun v
                            ⟹ adm (λx. u x ⊑ref v x)›
      and BOT_le_ref : ‹⋀Q. ⊥ ⊑ref Q›
      and cont_f : ‹cont f›
      and hyp : ‹⋀x. ∀Q ∈ ℛproc P. x ⊑ref Q ⟹ ∀Q ∈ ℛproc P. f x ⊑ref Q›
    shows ‹(μ X. f X) ⊑ref Q›
proof -
  have ‹∀Q ∈ ℛproc P. (μ X. f X) ⊑ref Q›
    apply (induct rule: fix_ind)
      apply (solves ‹simp add: adm_ref monofunI›)
     apply (solves ‹simp add: BOT_le_ref›)
    using hyp cont_f by auto
  with reachable show ‹(μ X. f X) ⊑ref Q› by blast
qed

lemma ℛproc_fix_ind_FD [consumes 1, case_names cont step]:
  ‹⟦Q ∈ ℛproc P; cont f; ⋀x Q. ∀Q ∈ ℛproc P. x ⊑FD Q ⟹ Q ∈ ℛproc P ⟹ f x ⊑FD Q⟧
   ⟹ (μ X. f X) ⊑FD Q›
  by (rule ℛproc_fix_ind) auto
    
 

―‹See what else we can add.›


subsection ‹Induction Proofs›


subsubsection ‹Generalizations›

―‹Again, new approach›

―‹TODO: reorganize this file›


(* put this somewhere else, maybe useful *)

lemma ‹Mprefix A P = Mprefix B Q ⟹ A = B›
  by (drule arg_cong[where f = initials]) (auto simp add: initials_Mprefix)    

lemma ‹Mndetprefix A P = Mprefix B Q ⟹ A = B›
  by (drule arg_cong[where f = initials]) (auto simp add: initials_Mprefix initials_Mndetprefix)

lemma ‹Mndetprefix A P = Mndetprefix B Q ⟹ A = B›
  by (drule arg_cong[where f = initials]) (auto simp add: initials_Mndetprefix)

(* end of block to move *)


print_context

lemma superset_initials_restriction_Mndetprefix_FD:
  ‹⊓a ∈ B → P a ⊑FD Q›
  if ‹⊓a ∈ A → P a ⊑FD Q› and ‹{e. ev e ∈ Q0} ⊆ B› and ‹A ≠ {} ∨ B = {}›
  supply that' = that(1)[unfolded failure_divergence_refine_def failure_refine_def divergence_refine_def]
proof (unfold failure_divergence_refine_def failure_refine_def divergence_refine_def, safe)
  from that'[THEN conjunct2] that(2)
  show ‹s ∈ 𝒟 Q ⟹ s ∈ 𝒟 (Mndetprefix B P)› for s
    by (simp add: D_Mndetprefix write0_def D_Mprefix subset_iff split: if_split_asm)
       (metis initials_memI D_T empty_iff)
next
  from that have that'' : ‹Q0 ⊆ ev ` A›
    using anti_mono_initials_FD initials_Mndetprefix by blast
  fix s X
  assume * : ‹(s, X) ∈ ℱ Q›
  with set_mp[OF that'[THEN conjunct1] this]
  consider ‹s = []› | e s' where ‹s = ev e # s'› ‹ev e ∈ Q0›
    by (simp add: F_Mndetprefix write0_def F_Mprefix split: if_split_asm)
       (metis initials_memI F_T)
  thus ‹(s, X) ∈ ℱ (Mndetprefix B P)›
  proof cases
    assume ‹s = []›
    hence ‹([], X ∪ (- Q0)) ∈ ℱ Q›
      by (metis "*" ComplD initials_memI is_processT5_S7' self_append_conv2)
    from set_mp[OF that'[THEN conjunct1] this] that'' that(2, 3)
    show ‹(s, X) ∈ ℱ (Mndetprefix B P)›
      by (simp add: ‹s = []› F_Mndetprefix write0_def F_Mprefix split: if_split_asm) blast
  next
    fix e s' assume ‹s = ev e # s'› ‹ev e ∈ Q0›
    with set_mp[OF that'[THEN conjunct1] "*"] that(2)
    show ‹(s, X) ∈ ℱ (Mndetprefix B P)›
      by (simp add: F_Mndetprefix write0_def F_Mprefix subset_iff split: if_split_asm) blast
  qed
qed

corollary initials_restriction_Mndetprefix_FD:
  ‹⊓a ∈ A → P a ⊑FD Q ⟹ ⊓a ∈ {e. ev e ∈ Q0} → P a ⊑FD Q›
  by (cases ‹A = {}›, simp add: STOP_FD_iff)
     (simp add: superset_initials_restriction_Mndetprefix_FD)

corollary events_of_restriction_Mndetprefix_FD:
  ‹⊓a ∈ A → P a ⊑FD (Q :: ('a, 'r) processptick) ⟹ ⊓a ∈ α(Q) → P a ⊑FD Q›
  by (cases ‹A = {}›, simp add: STOP_FD_iff)
     (erule superset_initials_restriction_Mndetprefix_FD,
      simp_all add: subset_iff initial_ev_imp_in_events_of)



lemma superset_initials_restriction_Mprefix_FD:
  ‹□a ∈ B → P a ⊑FD Q›
   if ‹□a ∈ A → P a ⊑FD Q› and ‹{e. ev e ∈ Q0} ⊆ B›
  and ‹B ⊆ A› ―‹Stronger assumption than with const‹Mndetprefix›.›
  supply that' = that(1)[unfolded failure_divergence_refine_def failure_refine_def divergence_refine_def]
proof (unfold failure_divergence_refine_def failure_refine_def divergence_refine_def, safe)
  from that'[THEN conjunct2] that(2)
  show ‹s ∈ 𝒟 Q ⟹ s ∈ 𝒟 (Mprefix B P)› for s
    by (simp add: D_Mprefix subset_iff image_iff)
       (metis initials_memI D_T)
next
  from that have that'' : ‹Q0 ⊆ ev ` A›
    using anti_mono_initials_FD initials_Mprefix by blast
  fix s X
  assume * : ‹(s, X) ∈ ℱ Q›
  with set_mp[OF that'[THEN conjunct1] this]
  consider ‹s = []› | ‹∃e s'. s = ev e # s' ∧ ev e ∈ Q0›
    by (simp add: F_Mprefix) (metis initials_memI F_T)
  thus ‹(s, X) ∈ ℱ (Mprefix B P)›
  proof cases
    assume ‹s = []›
    hence ‹([], X ∪ (- Q0)) ∈ ℱ Q›
      by (metis "*" ComplD initials_memI is_processT5_S7' self_append_conv2)
    from set_mp[OF that'[THEN conjunct1] this] that'' that(2, 3)
    show ‹(s, X) ∈ ℱ (Mprefix B P)› by (simp add: ‹s = []› F_Mprefix) blast
  next
    assume ‹∃e s'. s = ev e # s' ∧ ev e ∈ Q0›
    with set_mp[OF that'[THEN conjunct1] "*"] that(2)
    show ‹(s, X) ∈ ℱ (Mprefix B P)› by (auto simp add: F_Mprefix image_iff)
  qed
qed

corollary initials_restriction_Mprefix_FD:
  ‹{e. ev e ∈ Q0} ⊆ A ⟹ □a ∈ A → P a ⊑FD Q ⟹
   □a ∈ {e. ev e ∈ Q0} → P a ⊑FD Q›
  by (erule superset_initials_restriction_Mprefix_FD; simp)
 
corollary events_of_restriction_Mprefix_FD:
  ‹α(Q) ⊆ A ⟹ □a ∈ A → P a ⊑FD (Q :: ('a, 'r) processptick) ⟹
   □a ∈ α(Q) → P a ⊑FD Q›
  by (erule superset_initials_restriction_Mprefix_FD,
      simp add: subset_iff initial_ev_imp_in_events_of)



―‹This is much better with term‹(⊑DT)› refinement.›
lemma superset_initials_restriction_Mprefix_DT:
  ‹□a ∈ B → P a ⊑DT Q› if ‹□a ∈ A → P a ⊑DT Q› and ‹{e. ev e ∈ Q0} ⊆ B›
  supply that' = that(1)[unfolded trace_divergence_refine_def
                                  trace_refine_def divergence_refine_def]
proof (unfold trace_divergence_refine_def trace_divergence_refine_def
              trace_refine_def divergence_refine_def, safe)
  from that'[THEN conjunct2] that(2)
  show ‹s ∈ 𝒟 Q ⟹ s ∈ 𝒟 (Mprefix B P)› for s
    by (simp add: D_Mprefix subset_iff image_iff)
       (metis initials_memI D_T)
next
  from that have that'' : ‹Q0 ⊆ ev ` A›
    using anti_mono_initials_DT initials_Mprefix by blast
  fix s
  assume * : ‹s ∈ 𝒯 Q›
  with set_mp[OF that'[THEN conjunct1] this]
  consider ‹s = []› | ‹∃e s'. s = ev e # s' ∧ ev e ∈ Q0›
    by (simp add: T_Mprefix) (metis initials_memI)
  thus ‹s ∈ 𝒯 (Mprefix B P)›
  proof cases
    show ‹s = [] ⟹ s ∈ 𝒯 (Mprefix B P)› by simp
  next
    assume ‹∃e s'. s = ev e # s' ∧ ev e ∈ Q0›
    with set_mp[OF that'[THEN conjunct1] "*"] that(2)
    show ‹s ∈ 𝒯 (Mprefix B P)› by (auto simp add: T_Mprefix)
  qed
qed

corollary initials_restriction_Mprefix_DT:
  ‹□a ∈ A → P a ⊑DT Q ⟹ □a ∈ {e. ev e ∈ Q0} → P a ⊑DT Q›
  by (erule superset_initials_restriction_Mprefix_DT) simp
 
corollary events_restriction_Mprefix_DT:
  ‹□a ∈ A → P a ⊑DT (Q :: ('a, 'r) processptick) ⟹ □a ∈ α(Q) → P a ⊑DT Q›
  by (erule superset_initials_restriction_Mprefix_DT)
     (simp add: subset_iff initial_ev_imp_in_events_of)





paragraph ‹Admissibility›

(* lemma not_le_F_adm[simp]: 
  ‹adm (λx. ¬ u x ⊑F v x)› if ‹cont (u::('a::cpo) ⇒ 'b process)› and ‹monofun v›
proof (unfold adm_def, intro allI impI)
  fix Y
  assume chain : ‹chain Y› and hyp : ‹∀i. ¬ u (Y i) ⊑F v (Y i)›
  have ‹v (Y i) ⊑ v (⨆i. Y i)› for i by (simp add: chain is_ub_thelub monofunE that(2))
  from le_approx_lemma_F[OF this] have ‹¬ v (⨆i. Y i) ⊑F u (Y i)› for i 
    using hyp[rule_format, of i, unfolded failure_refine_def]

  have ‹(s, X) ∈ ℱ (v (⨆x. Y x)) ⟷ (∀i. (s, X) ∈ ℱ (v (Y i)))› for s X
    apply (simp add: lub_def)
  (* from hyp[unfolded failure_refine_def] have ‹› *)
    thm hyp[unfolded failure_refine_def subset_iff, simplified]
  
    thm limproc_is_thelub
  { fix s X
    assume ‹(s, X) ∈ ℱ (v (⨆x. Y x)) ⟹ (s, X) ∈ ℱ (u (⨆x. Y x))›
    hence False 
      using hyp[unfolded failure_refine_def subset_iff, simplified]
      apply (simp add: cont2contlubE limproc_is_thelub ch2ch_cont that(1) chain F_LUB)
      apply (auto simp add:   lub_def is_lub_def is_ub_def)
      
      find_theorems ‹(<<|)› name: def
      find_theorems monofun
      
      sorry }
  thus ‹¬ u (Lub Y) ⊑F v (Lub Y)› 
    oops
    unfolding failure_refine_def apply simp by (auto simp add: subset_iff) *)
―‹See if we can do this kind of version with const‹monofun›, not easy.›



―‹Less powerful versions›
lemma not_le_F_adm[simp]: ‹cont u ⟹ adm (λx. ¬ u x ⊑F P)›
  by (simp add: adm_def cont2contlubE ch2ch_cont failure_refine_def
                limproc_is_thelub F_LUB subset_iff) blast

lemma not_le_T_adm[simp]: ‹cont u ⟹ adm (λx. ¬ u x ⊑T P)›
  by (simp add: adm_def cont2contlubE ch2ch_cont trace_refine_def
                limproc_is_thelub T_LUB subset_iff) blast

lemma not_le_D_adm[simp]: ‹cont u ⟹ adm (λx. ¬ u x ⊑D P)›
  by (simp add: adm_def cont2contlubE ch2ch_cont divergence_refine_def
                limproc_is_thelub D_LUB subset_iff) blast

lemma not_le_FD_adm[simp]: ‹cont u ⟹ adm (λx. ¬ u x ⊑FD P)›
  by (simp add: adm_def cont2contlubE ch2ch_cont failure_divergence_refine_def 
                failure_refine_def divergence_refine_def limproc_is_thelub F_LUB D_LUB subset_iff) blast

lemma not_le_DT_adm[simp]: ‹cont u ⟹ adm (λx. ¬ u x ⊑DT P)›
  by (simp add: adm_def cont2contlubE ch2ch_cont trace_divergence_refine_def trace_refine_def
                divergence_refine_def limproc_is_thelub D_LUB T_LUB subset_iff) blast





lemma initials_refusal: 
   ‹(t, UNIV) ∈ ℱ P› if assms: ‹t ∈ 𝒯 P› ‹tF t› ‹(t, (P after𝒯 t)0) ∈ ℱ P›
proof (rule ccontr)
  assume ‹(t, UNIV) ∉ ℱ P›
  from is_processT5_S7'[OF assms(3), of UNIV, simplified, OF this]
  obtain e where ‹e ∉ (P after𝒯 t)0 ∧ t @ [e] ∈ 𝒯 P› ..
  thus False by (simp add: initials_def T_Aftertrace_eq assms(1, 2))
qed




lemma leF_ev_initialE' :
  assumes ‹STOP ⊓ (⊓a ∈ UNIV → P a) ⊑F Q› ‹Q ≠ STOP› obtains a where ‹ev a ∈ Q0›
proof -
  from ‹Q ≠ STOP› initials_empty_iff_STOP obtain e where ‹e ∈ Q0› by blast
  with ‹STOP ⊓ (⊓a ∈ UNIV → P a) ⊑F Q› obtain a where ‹e = ev a›
    by (auto simp add: failure_refine_def F_Ndet F_STOP F_Mndetprefix'
                intro: T_F dest!: initials_memD)
  with ‹e ∈ Q0› that show thesis by blast
qed

corollary leF_ev_initialE :
  assumes ‹⊓a ∈ UNIV → P a ⊑F Q› obtains a where ‹ev a ∈ Q0›
proof -
  from ‹⊓a ∈ UNIV → P a ⊑F Q› Ndet_F_self_right trans_F
  have ‹STOP ⊓ (⊓a ∈ UNIV → P a) ⊑F Q› by blast
  moreover from ‹⊓a ∈ UNIV → P a ⊑F Q› have ‹Q ≠ STOP›
    by (auto simp add: Process_eq_spec failure_refine_def F_Mndetprefix' F_STOP)
  ultimately obtain a where ‹ev a ∈ Q0› by (rule leF_ev_initialE')
  with that show thesis by blast
qed
  

lemma leFD_ev_initialE' :
  ‹STOP ⊓ (⊓a ∈ UNIV → P a) ⊑FD Q ⟹ Q ≠ STOP ⟹ (⋀a. ev a ∈ Q0 ⟹ thesis) ⟹ thesis›
  by (meson leFD_imp_leF leF_ev_initialE')

lemma leFD_ev_initialE : 
  ‹⊓a ∈ UNIV → P a ⊑FD Q ⟹ (⋀a. ev a ∈ Q0 ⟹ thesis) ⟹ thesis›
  by (meson leFD_imp_leF leF_ev_initialE)
    
 
(* TODO: useful ? *)
method prove_propagation uses simp base =
       induct rule: reachable_processes_FD_refinement_propagation_induct,
       solves simp, solves ‹use base in ‹simp add: simp››, solves ‹simp add: simp›




text ‹The three following results illustrate how powerful are our new rules of induction.›

text ‹Really ? The second version with @{thm cont_parallel_fix_ind} seems easier...›

lemma (* deadlock_free_imp_DF_F_prem: *)
  ‹Q ∈ ℛproc P ⟹ DF α(P) ⊑F Q› if df_P: ‹deadlock_free P›
proof (unfold DF_def, induct rule: reachable_processes_fix_ind_F)
  show ‹cont (λx. ⊓ a ∈ events_of P → x)› by simp
next
  fix x
  assume hyp : ‹∀Q ∈ ℛproc P. x ⊑F Q›
  show ‹s ∈ 𝒯 P ⟹ tickFree s ⟹ ⊓a ∈ events_of P → x ⊑F P after𝒯 s› for s
  proof (unfold failure_refine_def, safe)
    show ‹s ∈ 𝒯 P ⟹ tickFree s ⟹ (t, X) ∈ ℱ (P after𝒯 s) ⟹ 
          (t, X) ∈ ℱ (⊓a ∈ events_of P → x)› for t X
    proof (induct t arbitrary: s)
      case Nil
      have * : ‹deadlock_free (P after𝒯 s)›
        by (metis Aftertrace.simps(1) ‹s ∈ 𝒯 P› deadlock_free_Aftertrace_characterization df_P)
      have ‹([], X ∪ (- initials (P after𝒯 s))) ∈ ℱ (P after𝒯 s)›
        by (metis ComplD Nil.prems T_Aftertrace_eq is_processT5_S7' 
                  mem_Collect_eq initials_Aftertrace self_append_conv2)
      from this[THEN set_rev_mp, OF "*"[unfolded deadlock_free_F failure_refine_def]]
      show ‹([], X) ∈ ℱ (⊓a ∈ events_of P → x)›
        apply (subst (asm) F_DF, simp add: F_Mndetprefix write0_def F_Mprefix image_iff)
        using Nil.prems(1) deadlock_free_implies_non_terminating events_of_iff_reachable_ev 
              reachable_ev_iff_in_initials_Aftertrace_for_some_tickFree_T that by blast
    next
      case (Cons e t)
      from Cons.prems(1, 2) have * : ‹P after𝒯 s ∈ ℛproc P›
        by (auto simp add: reachable_processes_is)
      obtain e' where ** : ‹e = ev e'› ‹e' ∈ events_of P›
        by (meson Cons.prems(1, 3) initials_memI F_T set_mp
                  deadlock_free_implies_non_terminating df_P imageE 
                  non_terminating_is_right initials_Aftertrace_subset_events_of)
      from Cons.prems F_Aftertrace_eq "**"(1)
      have ‹(t, X) ∈ ℱ (P after𝒯 (s @ [e]))› by (simp add: F_Aftertrace)
      also have ‹… ⊆ ℱ x›
        apply (rule hyp[rule_format, unfolded failure_refine_def,
                        of ‹P after𝒯 (s @ [e])›, simplified])
        apply (simp add: Aftertrace_snoc "**"(1) Aftertick_def)
        apply (rule reachable_after[OF "*" ])
        using Cons.prems(3) initials_memI F_T "**"(1) by blast
      finally have ‹(t, X) ∈ ℱ x› .
      with "**" show ?case by (auto simp add: F_Mndetprefix write0_def F_Mprefix)
    qed
  qed
qed


lemma (* deadlock_freeSKIPS_imp_DFSKIPS_F_prem: *)
  ‹Q ∈ ℛproc P ⟹ DFSKIPS α(P) UNIV ⊑F Q› if dfSKIP_P: ‹deadlock_freeSKIPS P›
proof (unfold DFSKIPS_def, induct rule: reachable_processes_fix_ind_F)
  show ‹cont (λx. (⊓a ∈ events_of P → x) ⊓ SKIPS UNIV)› by simp
next
  fix x
  assume hyp : ‹∀Q ∈ ℛproc P. x ⊑F Q›
  show ‹s ∈ 𝒯 P ⟹ tickFree s ⟹ (⊓a ∈ events_of P → x) ⊓ SKIPS UNIV ⊑F P after𝒯 s› for s
  proof (unfold failure_refine_def, safe)
    show ‹s ∈ 𝒯 P ⟹ tickFree s ⟹ (t, X) ∈ ℱ (P after𝒯 s) ⟹
          (t, X) ∈ ℱ ((⊓a ∈ events_of P → x) ⊓ SKIPS UNIV)› for t X
    proof (induct t arbitrary: s)
      case Nil
      have * : ‹deadlock_freeSKIPS (P after𝒯 s)›
        by (metis Aftertrace.simps(1) Nil.prems(1, 2) deadlock_freeSKIPS_Aftertrace_characterization dfSKIP_P)
      have ‹([], X ∪ (- initials (P after𝒯 s))) ∈ ℱ (P after𝒯 s)›
        by (metis (no_types, opaque_lifting) ComplD initials_memI
                  Nil.prems(3) append_eq_Cons_conv is_processT5_S7')
      from this[THEN set_rev_mp, OF "*"[unfolded deadlock_freeSKIPS_def failure_refine_def]]
      show ‹([], X) ∈ ℱ ((⊓a ∈ events_of P → x) ⊓ SKIPS UNIV)›
        apply (subst (asm) F_DFSKIPS, simp add: F_Ndet F_SKIPS F_Mndetprefix write0_def F_Mprefix image_iff)
        using Nil.prems(1, 2) events_of_iff_reachable_ev
              reachable_ev_iff_in_initials_Aftertrace_for_some_tickFree_T by blast
    next
      case (Cons e t)
      from Cons.prems(1, 2) have * : ‹P after𝒯 s ∈ ℛproc P›
        by (auto simp add: reachable_processes_is)
      have ‹deadlock_freeSKIPS (P after𝒯 s)›
        by (metis Aftertrace.simps(1) Cons.prems(1, 2) deadlock_freeSKIPS_Aftertrace_characterization dfSKIP_P)
      then consider a where ‹e = ev a› ‹a ∈ events_of P› | r where ‹e = ✓(r)›
        unfolding deadlock_freeSKIPS_def failure_refine_def
        apply (subst (asm) F_DFSKIPS, simp add: subset_iff image_iff)
        by (metis reachable_ev_iff_in_initials_Aftertrace_for_some_tickFree_T Cons.prems
                  initials_memI F_T events_of_iff_reachable_ev list.distinct(1) list.sel(1))
      thus ?case
      proof cases
        fix a assume ** : ‹e = ev a› ‹a ∈ events_of P›
        from Cons.prems F_Aftertrace "**"(1)
        have ‹(t, X) ∈ ℱ (P after𝒯 (s @ [e]))› by (simp add: F_Aftertrace_eq)
        also have ‹… ⊆ ℱ x›
          apply (rule hyp[rule_format, unfolded failure_refine_def,
                        of ‹P after𝒯 (s @ [e])›, simplified])
          apply (simp add: Aftertrace_snoc "**"(1) Aftertick_def)
          apply (rule reachable_after[OF "*" ])
          using Cons.prems(3) initials_memI F_T "**"(1) by blast
        finally have ‹(t, X) ∈ ℱ x› .
        with "**" show ?case by (auto simp add: F_Ndet F_Mndetprefix write0_def F_Mprefix)
      next
        fix r assume ‹e = ✓(r)›
        hence ‹t = []›
          by (metis Cons.prems(3) F_imp_front_tickFree eventptick.disc(2) front_tickFree_Cons_iff)
        thus ?case by (simp add: ‹e = ✓(r)› F_Ndet F_SKIPS)
      qed
    qed
  qed
qed


context fixes P :: ‹('a, 'r) processptick› begin

theorem deadlock_free_iff_empty_ticks_of_and_deadlock_freeSKIPS :
  ‹deadlock_free P ⟷ ✓s(P) = {} ∧ deadlock_freeSKIPS P›
proof (intro iffI conjI)
  from deadlock_free_implies_non_terminating tickFree_traces_iff_empty_ticks_of
  show ‹deadlock_free P ⟹ ✓s(P) = {}› by fast
next
  show ‹deadlock_free P ⟹ deadlock_freeSKIPS P›
    by (fact deadlock_free_imp_deadlock_freeSKIPS)
next
  have ‹Q ∈ ℛproc P ⟹ DFSKIPS UNIV UNIV ⊑F Q ⟹ DF UNIV ⊑F Q› if ‹✓s(P) = {}› for Q
  proof (unfold DF_def DFSKIPS_def, induct arbitrary: Q rule: cont_parallel_fix_ind)
    show ‹cont (λx. (⊓a∈UNIV → x) ⊓ SKIPS UNIV)› by simp
  next
    show ‹cont (λx. ⊓a∈UNIV → x)› by simp
  next
    show ‹adm (λx. ∀Q. Q ∈ ℛproc P ⟶ fst x ⊑F Q ⟶ snd x ⊑F Q)› by simp
  next
    show ‹⋀Q. ⊥ ⊑F Q› by simp
  next
    fix x y Q assume hyp : ‹Q ∈ ℛproc P ⟹ x ⊑F Q ⟹ y ⊑F Q› for Q
    assume ‹Q ∈ ℛproc P› ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q›
    from ‹✓s(P) = {}› ‹Q ∈ ℛproc P› have ‹✓s(Q) = {}›
      using ticks_of_reachable_processes_subset by auto

    from ‹✓s(Q) = {}› initial_tick_imp_in_ticks_of have ‹{r. ✓(r) ∈ Q0} = {}› by force
    moreover from ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q›
    have ‹Q0 ≠ {}› by (auto simp add: initials_empty_iff_STOP Process_eq_spec failure_refine_def
                                      F_Ndet F_Mndetprefix' F_SKIPS subset_iff F_STOP) 
    ultimately have ‹{a. ev a ∈ Q0} ≠ {}›
      by (metis empty_Collect_eq equals0I eventptick.exhaust)
    hence ‹⊓a ∈ UNIV → y ⊑F ⊓a ∈ {a. ev a ∈ Q0} → y›
      by (metis Mndetprefix_F_subset top_greatest)
    moreover have ‹… ⊑F ⊓a ∈ {a. ev a ∈ Q0} → Q after a›
    proof (rule mono_Mndetprefix_F, clarify, rule hyp)
      show ‹ev a ∈ Q0 ⟹ Q after a ∈ ℛproc P› for a
        by (simp add: ‹Q ∈ ℛproc P› reachable_after)
    next
      show ‹ev a ∈ Q0 ⟹ x ⊑F Q after a› for a
        by (frule mono_After_F[OF _ ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q›])
           (simp add: After_Ndet initials_Mndetprefix image_iff After_Mndetprefix)
    qed
    moreover have ‹… ⊑F Q›
    proof (unfold failure_refine_def, safe)
      show ‹(t, X) ∈ ℱ (⊓a ∈ {a. ev a ∈ Q0} → Q after a)› if ‹(t, X) ∈ ℱ Q› for t X
      proof (cases t)
        from initial_tick_imp_in_ticks_of ‹✓s(Q) = {}› have ‹range tick ⊆ - Q0› by force
        assume ‹t = []›
        with ‹(t, X) ∈ ℱ Q› have ‹([], X ∪ - Q0) ∈ ℱ Q›
          by (metis ComplD initials_memI is_processT5_S7' self_append_conv2)
        with ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q›
        show ‹(t, X) ∈ ℱ (⊓a ∈ {a. ev a ∈ Q0} → Q after a)›
          by (simp add: failure_refine_def F_Ndet F_SKIPS ‹t = []› F_Mndetprefix' subset_iff)
             (meson Compl_iff UnI1 UnI2 ‹range tick ⊆ - Q0› list.distinct(1) range_subsetD)
      next
        from ‹(t, X) ∈ ℱ Q› ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q› ‹{a. ev a ∈ Q0} ≠ {}› ‹✓s(Q) = {}›
        show ‹t = e # t' ⟹ (t, X) ∈ ℱ (⊓a ∈ {a. ev a ∈ Q0} → Q after a)› for e t'
          by (simp add: failure_refine_def F_Ndet F_SKIPS F_Mndetprefix' F_After subset_iff)
             (metis F_T empty_iff eventptick.exhaust initial_tick_imp_in_ticks_of initials_memI)
      qed
    qed
    ultimately show ‹⊓a ∈ UNIV → y ⊑F Q› using trans_F by blast
  qed
  thus ‹✓s(P) = {} ∧ deadlock_freeSKIPS P ⟹ deadlock_free P›
    by (simp add: reachable_self deadlock_freeSKIPS_def deadlock_free_F)
qed



lemma reachable_processes_DF_UNIV_leF_imp_DF_events_of_leF :
  ‹Q ∈ ℛproc P ⟹ DF UNIV ⊑F Q ⟹ DF α(P) ⊑F Q› for Q
proof (unfold DF_def, induct arbitrary: Q rule: cont_parallel_fix_ind)
  show ‹cont (λx. ⊓a ∈ UNIV → x)› by simp
next
  show ‹cont (λx. ⊓a ∈ α(P) → x)› by simp
next
  show ‹adm (λx. ∀Q. Q ∈ ℛproc P ⟶ fst x ⊑F Q ⟶ snd x ⊑F Q)› by simp
next
  show ‹⋀Q. ⊥ ⊑F Q› by simp
next
  fix x y Q assume hyp : ‹Q ∈ ℛproc P ⟹ x ⊑F Q ⟹ y ⊑F Q› for Q
  assume ‹Q ∈ ℛproc P› and ‹⊓a ∈ UNIV → x ⊑F Q›

  from ‹⊓a ∈ UNIV → x ⊑F Q› obtain a where ‹ev a ∈ Q0› by (elim leF_ev_initialE)

  have ‹⊓a ∈ α(P) → y ⊑F ⊓a ∈ {a. ev a ∈ Q0} → y›
    by (metis (mono_tags, lifting) Mndetprefix_F_subset ‹Q ∈ ℛproc P›
              ‹ev a ∈ Q0› empty_iff events_of_reachable_processes_subset
              initial_ev_imp_in_events_of mem_Collect_eq subset_iff)
  moreover have ‹… ⊑F ⊓a ∈ {a. ev a ∈ Q0} → Q after a›
  proof (rule mono_Mndetprefix_F, clarify)
    show ‹ev a ∈ Q0 ⟹ y ⊑F Q after a› for a
      by (metis mono_After_F After_Mndetprefix UNIV_I ‹Q ∈ ℛproc P›
                ‹⊓a∈UNIV → x ⊑F Q› hyp reachable_processes.simps)
  qed
  moreover have ‹… ⊑F Q›
  proof (unfold failure_refine_def, safe)
    show ‹(t, X) ∈ ℱ (⊓a ∈ {a. ev a ∈ Q0} → Q after a)› if ‹(t, X) ∈ ℱ Q› for t X
    proof (cases t)
      assume ‹t = []›
      with ‹(t, X) ∈ ℱ Q› have ‹([], X ∪ (- Q0)) ∈ ℱ Q›
        by (metis ComplD initials_memI is_processT5_S7' self_append_conv2)
      from ‹⊓a ∈ UNIV → x ⊑F Q› ‹([], X ∪ (- Q0)) ∈ ℱ Q› have ‹¬ range ev ⊆ X ∪ - Q0›
        by (simp add: failure_refine_def F_Mndetprefix' subset_iff) blast
      then obtain b where ‹ev b ∈ Q0› ‹ev b ∉ X› by auto
      with ‹t = []› ‹ev a ∈ Q0› show ‹(t, X) ∈ ℱ (⊓a ∈ {a. ev a ∈ Q0} → Q after a)›
        by (auto simp add: F_Mndetprefix')
    next
      from ‹⊓a ∈ UNIV → x ⊑F Q› ‹(t, X) ∈ ℱ Q› ‹ev a ∈ Q0›
      show ‹t = e # t' ⟹ (t, X) ∈ ℱ (⊓a ∈ {a. ev a ∈ Q0} → Q after a)› for e t'
        by (auto simp add: failure_refine_def F_Mndetprefix' F_After intro!: F_T initials_memI)
    qed
  qed
  ultimately show ‹⊓a ∈ α(P) → y ⊑F Q› using trans_F by blast
qed


lemma reachable_processes_CHAOS_UNIV_leF_imp_CHAOS_events_of_leF :
  ‹Q ∈ ℛproc P ⟹ CHAOS UNIV ⊑F Q ⟹ CHAOS α(P) ⊑F Q› for Q
proof (unfold CHAOS_def, induct arbitrary: Q rule: cont_parallel_fix_ind)
  show ‹cont (λx. STOP ⊓ (□a ∈ UNIV → x))› by simp
next
  show ‹cont (λx. STOP ⊓ (□a ∈ α(P) → x))› by simp
next
  show ‹adm (λx. ∀Q. Q ∈ ℛproc P ⟶ fst x ⊑F Q ⟶ snd x ⊑F Q)› by simp
next
  show ‹⋀Q. ⊥ ⊑F Q› by simp
next
  fix x y Q assume hyp : ‹Q ∈ ℛproc P ⟹ x ⊑F Q ⟹ y ⊑F Q› for Q
  assume ‹Q ∈ ℛproc P› and ‹STOP ⊓ (□a∈UNIV → x) ⊑F Q›

  from ‹Q ∈ ℛproc P› events_of_reachable_processes_subset initial_ev_imp_in_events_of
  have ‹STOP ⊓ (□a ∈ α(P) → y) ⊑F STOP ⊓ (□a ∈ {a. ev a ∈ Q0} → y)›
    by (fastforce simp add: failure_refine_def Ndet_projs Mprefix_projs STOP_projs)
  moreover have ‹… ⊑F STOP ⊓ (□a ∈ {a. ev a ∈ Q0} → Q after a)›
  proof (intro mono_Ndet_F[OF idem_F] mono_Mprefix_F, clarify)
    show ‹ev a ∈ Q0 ⟹ y ⊑F Q after a› for a
      by (frule mono_After_F[OF _ ‹STOP ⊓ (□a∈UNIV → x) ⊑F Q›])
         (simp add: After_Ndet initials_Mprefix After_Mprefix
                    ‹Q ∈ ℛproc P› hyp reachable_after)
  qed
  moreover have ‹… ⊑F Q›
  proof (unfold failure_refine_def, safe)
    from ‹STOP ⊓ (□a∈UNIV → x) ⊑F Q›
    show ‹(t, X) ∈ ℱ Q ⟹ (t, X) ∈ ℱ (STOP ⊓ (□a ∈ {a. ev a ∈ Q0} → Q after a))› for t X
      by (auto simp add: refine_defs F_Ndet F_Mprefix F_After intro!: F_T initials_memI)
  qed
  ultimately show ‹STOP ⊓ (□a ∈ α(P) → y) ⊑F Q› using trans_F by blast
qed


lemma reachable_processes_CHAOSSKIPS_UNIV_UNIV_leF_imp_CHAOS_events_of_ticks_of_leFD :
  ‹Q ∈ ℛproc P ⟹ CHAOSSKIPS UNIV UNIV ⊑FD Q ⟹ CHAOSSKIPS α(P) ✓s(P) ⊑FD Q› for Q
proof (unfold CHAOSSKIPS_def, induct arbitrary: Q rule: cont_parallel_fix_ind)
  show ‹cont (λx. SKIPS UNIV ⊓ STOP ⊓ (□a ∈ UNIV → x))› by simp
next
  show ‹cont (λx. SKIPS ✓s(P) ⊓ STOP ⊓ (□a ∈ α(P) → x))› by simp
next
  show ‹adm (λx. ∀Q. Q ∈ℛproc P ⟶ fst x ⊑FD Q ⟶ snd x ⊑FD Q)› by simp
next
  show ‹⋀Q. ⊥ ⊑FD Q› by simp
next
  fix x y Q assume hyp : ‹Q ∈ ℛproc P ⟹ x ⊑FD Q ⟹ y ⊑FD Q› for Q
  assume ‹Q ∈ ℛproc P› and ‹SKIPS UNIV ⊓ STOP ⊓ (□a ∈ UNIV → x) ⊑FD Q›

  from ‹Q ∈ ℛproc P› ticks_of_reachable_processes_subset initial_tick_imp_in_ticks_of
  have ‹SKIPS ✓s(P) ⊓ STOP ⊑FD SKIPS {r. ✓(r) ∈ Q0} ⊓ STOP›
    by (fastforce simp add: refine_defs Ndet_projs STOP_projs SKIPS_projs)
  moreover from ‹Q ∈ ℛproc P› events_of_reachable_processes_subset initial_ev_imp_in_events_of
  have ‹STOP ⊓ (□a ∈ α(P) → y) ⊑FD STOP ⊓ (□a ∈ {a. ev a ∈ Q0} → y)›
    by (fastforce simp add: refine_defs Ndet_projs STOP_projs Mprefix_projs)
  ultimately have ‹SKIPS ✓s(P) ⊓ STOP ⊓ (□a ∈ α(P) → y) ⊑FD
                   SKIPS {r. ✓(r) ∈ Q0} ⊓ STOP ⊓ (□a ∈ {a. ev a ∈ Q0} → y)›
    by (auto simp add: refine_defs Ndet_projs)
  moreover have ‹… ⊑FD SKIPS {r. ✓(r) ∈ Q0} ⊓ STOP ⊓ (□a ∈ {a. ev a ∈ Q0} → Q after a)›
  proof (intro mono_Ndet_FD[OF idem_FD] mono_Mprefix_FD, clarify)
    show ‹ev a ∈ Q0 ⟹ y ⊑FD Q after a› for a
      by (frule mono_After_FD[OF _ ‹SKIPS UNIV ⊓ STOP ⊓ (□a ∈ UNIV → x) ⊑FD Q›])
         (simp add: After_Ndet initials_Mprefix initials_Ndet image_iff
                    After_Mprefix ‹Q ∈ ℛproc P› hyp reachable_after)
  qed
  moreover have ‹… ⊑FD Q›
  proof (unfold refine_defs, safe)
    from ‹SKIPS UNIV ⊓ STOP ⊓ (□a ∈ UNIV → x) ⊑FD Q›
    show ‹t ∈ 𝒟 Q ⟹ t ∈ 𝒟 (SKIPS {r. ✓(r) ∈ Q0} ⊓ STOP ⊓ (□a ∈ {a. ev a ∈ Q0} → Q after a))› for t
      by (auto simp add: refine_defs D_Ndet D_Mprefix D_STOP D_After D_SKIPS)
         (use D_T initials_memI in blast)
  next
    from ‹SKIPS UNIV ⊓ STOP ⊓ (□a ∈ UNIV → x) ⊑FD Q›
    show ‹(t, X) ∈ ℱ Q ⟹ (t, X) ∈ ℱ (SKIPS {r. ✓(r) ∈ Q0} ⊓ STOP ⊓ (□a ∈ {a. ev a ∈ Q0} → Q after a))› for t X
      by (cases t, simp_all add: refine_defs F_Ndet F_Mprefix F_After F_SKIPS F_STOP)
         (use F_T initials_memI in blast)
  qed
  ultimately show ‹SKIPS ✓s(P) ⊓ STOP ⊓ (□a ∈ α(P) → y) ⊑FD Q› by force
qed



theorem deadlock_free_iff_DF_events_of_leF :
  ‹deadlock_free P ⟷ α(P) ≠ {} ∧ DF α(P) ⊑F P›
proof (intro iffI conjI)
  show ‹α(P) ≠ {} ∧ DF α(P) ⊑F P ⟹ deadlock_free P›
    by (meson DF_Univ_freeness deadlock_free_F order_refl trans_F)
next
  show ‹deadlock_free P ⟹ α(P) ≠ {}› by (simp add: nonempty_events_of_if_deadlock_free)
next
  show ‹deadlock_free P ⟹ DF α(P) ⊑F P›
    by (simp add: deadlock_free_F reachable_self
                  reachable_processes_DF_UNIV_leF_imp_DF_events_of_leF)
qed

corollary deadlock_free_iff_DF_events_of_leFD :
  ‹deadlock_free P ⟷ α(P) ≠ {} ∧ DF α(P) ⊑FD P›
  by (metis deadlock_free_iff_DF_events_of_leF deadlock_free_def div_free_DF
            divergence_refine_def failure_divergence_refine_def)

corollary deadlock_free_iff_DF_strict_events_of_leF :
  ‹deadlock_free P ⟷ α(P) ≠ {} ∧ DF α(P) ⊑F P› 
  by (metis anti_mono_events_of_F deadlock_free_iff_DF_events_of_leF
            deadlock_free_implies_div_free events_of_DF events_of_is_strict_events_of_or_UNIV
            order_class.order_eq_iff strict_events_of_subset_events_of)

corollary deadlock_free_iff_DF_strict_events_of_leFD :
  ‹deadlock_free P ⟷ α(P) ≠ {} ∧ DF α(P) ⊑FD P›
 by (metis DF_Univ_freeness deadlock_free_iff_DF_events_of_leFD
            deadlock_free_implies_div_free events_of_is_strict_events_of_or_UNIV)



theorem lifelock_free_iff_CHAOS_events_of_leF :
  ‹lifelock_free P ⟷ CHAOS α(P) ⊑F P›
proof (intro iffI conjI)
  show ‹CHAOS α(P) ⊑F P ⟹ lifelock_free P›
    by (meson CHAOS_subset_FD lifelock_free_def non_terminating_F
              non_terminating_FD top_greatest trans_F)
next
  show ‹lifelock_free P ⟹ CHAOS α(P) ⊑F P›
    by (simp add: leFD_imp_leF lifelock_free_def reachable_self
                  reachable_processes_CHAOS_UNIV_leF_imp_CHAOS_events_of_leF)
qed

corollary lifelock_free_iff_CHAOS_strict_events_of_leF :
  ‹lifelock_free P ⟷ CHAOS α(P) ⊑F P›
  by (metis anti_mono_ticks_of_F bot.extremum_uniqueI empty_not_UNIV
      events_of_is_strict_events_of_or_UNIV lifelock_free_iff_CHAOS_events_of_leF
      ticks_CHAOS ticks_of_is_strict_ticks_of_or_UNIV)

corollary lifelock_free_iff_CHAOS_events_of_leFD :
  ‹lifelock_free P ⟷ CHAOS α(P) ⊑FD P›
  by (metis div_free_CHAOS divergence_refine_def failure_divergence_refine_def
            lifelock_free_def lifelock_free_iff_CHAOS_events_of_leF)

corollary lifelock_free_iff_CHAOS_strict_events_of_leFD :
  ‹lifelock_free P ⟷ CHAOS α(P) ⊑FD P›
  by (metis anti_mono_events_of_F antisym events_of_CHAOS leFD_imp_leF
      lifelock_free_iff_CHAOS_events_of_leFD
      lifelock_free_iff_CHAOS_strict_events_of_leF strict_events_of_subset_events_of)





theorem lifelock_freeSKIPS_iff_CHAOSSKIPS_events_of_ticks_of_FD :
  ‹lifelock_freeSKIPS P ⟷ CHAOSSKIPS α(P) ✓s(P) ⊑FD P›
proof (intro iffI)
  show ‹CHAOSSKIPS α(P) ✓s(P) ⊑FD P ⟹ lifelock_freeSKIPS P›
    by (metis events_of_is_strict_events_of_or_UNIV lifelock_freeSKIPS_def
              lifelock_freeSKIPS_iff_div_free ticks_of_is_strict_ticks_of_or_UNIV)
next
  show ‹lifelock_freeSKIPS P ⟹ CHAOSSKIPS α(P) ✓s(P) ⊑FD P›
    by (simp add: lifelock_freeSKIPS_def reachable_self
                  reachable_processes_CHAOSSKIPS_UNIV_UNIV_leF_imp_CHAOS_events_of_ticks_of_leFD)
qed

corollary lifelock_freeSKIPS_iff_CHAOSSKIPS_strict_events_of_strict_ticks_of_FD :
  ‹lifelock_freeSKIPS P ⟷ CHAOSSKIPS α(P) ✓s(P) ⊑FD P›
  by (metis (no_types) anti_mono_events_of_FD anti_mono_ticks_of_FD events_of_CHAOSSKIPS
      events_of_is_strict_events_of_or_UNIV lifelock_freeSKIPS_iff_CHAOSSKIPS_events_of_ticks_of_FD
      lifelock_freeSKIPS_iff_div_free ticks_CHAOSSKIPS ticks_of_is_strict_ticks_of_or_UNIV top.extremum_uniqueI)

   

theorem deadlock_freeSKIPS_iff_DFSKIPS_events_of_ticks_of_leF :
  ‹deadlock_freeSKIPS P ⟷ (  if α(P) = {} ∧ ✓s(P) = {} then False
                            else   if ✓s(P) = {} then DF α(P) ⊑F P
                                 else   if α(P) = {} then SKIPS ✓s(P) ⊑F P
                                      else DFSKIPS α(P) ✓s(P) ⊑F P)›
  (is ‹_ ⟷ ?rhs›)
proof (split if_split, intro conjI impI)
  from deadlock_free_iff_empty_ticks_of_and_deadlock_freeSKIPS nonempty_events_of_if_deadlock_free
  show ‹α(P) = {} ∧ ✓s(P) = {} ⟹ deadlock_freeSKIPS P ⟷ False› by blast
next
  assume ‹¬ (α(P) = {} ∧ ✓s(P) = {})›
  show ‹deadlock_freeSKIPS P ⟷
        (  if ✓s(P) = {} then DF α(P) ⊑F P
         else if α(P) = {} then SKIPS ✓s(P) ⊑F P else DFSKIPS α(P) ✓s(P) ⊑F P)›
  proof (split if_split, intro conjI impI)
    from ‹¬ (α(P) = {} ∧ ✓s(P) = {})› deadlock_free_iff_DF_events_of_leF
         deadlock_free_iff_empty_ticks_of_and_deadlock_freeSKIPS 
    show ‹✓s(P) = {} ⟹ deadlock_freeSKIPS P ⟷ DF α(P) ⊑F P› by blast
  next
    show ‹deadlock_freeSKIPS P ⟷
          (if α(P) = {} then SKIPS ✓s(P) ⊑F P else DFSKIPS α(P) ✓s(P) ⊑F P)› if ‹✓s(P) ≠ {}›
    proof (split if_split, intro conjI impI)
      assume ‹α(P) = {}›
      with initial_ev_imp_in_events_of have ‹range ev ⊆ - P0› by force
      show ‹deadlock_freeSKIPS P ⟷ SKIPS ✓s(P) ⊑F P›
      proof (rule iffI)
        show ‹SKIPS ✓s(P) ⊑F P ⟹ deadlock_freeSKIPS P›
          by (metis deadlock_freeSKIPS_SKIPS deadlock_freeSKIPS_def ‹✓s(P) ≠ {}› trans_F)
      next
        show ‹SKIPS ✓s(P) ⊑F P› if ‹deadlock_freeSKIPS P›
        proof (unfold failure_refine_def, safe)
          show ‹(t, X) ∈ ℱ (SKIPS ✓s(P))› if ‹(t, X) ∈ ℱ P› for t X
          proof (cases t)
            assume ‹t = []›
            with ‹(t, X) ∈ ℱ P› have ‹(t, X ∪ - P0) ∈ ℱ P›
              by (metis ComplD initials_memI is_processT5_S7' self_append_conv2)
            with ‹deadlock_freeSKIPS P› have ‹(t, X ∪ - P0) ∈ ℱ (DFSKIPS UNIV UNIV)›
              by (auto simp add: deadlock_freeSKIPS_def failure_refine_def)
            with ‹range ev ⊆ - P0› ‹✓s(P) ≠ {}› show ‹(t, X) ∈ ℱ (SKIPS ✓s(P))›
              by (subst (asm) DFSKIPS_unfold)
                 (auto simp add: F_Ndet F_Mndetprefix' F_SKIPS ‹t = []›
                          intro: initial_tick_imp_in_ticks_of)
          next
            fix e t' assume ‹t = e # t'›
            with F_T ‹(t, X) ∈ ℱ P› ‹α(P) = {}› obtain r where ‹r ∈ ✓s(P)› ‹e = ✓(r)› ‹t' = []›
              by (metis F_imp_front_tickFree empty_iff eventptick.exhaust events_of_memI
                        front_tickFree_Cons_iff initial_tick_imp_in_ticks_of
                        initials_memI is_ev_def list.set_intros(1))
            thus ‹(t, X) ∈ ℱ (SKIPS ✓s(P))›
              by (simp add: F_Mndetprefix' F_SKIPS ‹✓s(P) ≠ {}› ‹t = e # t'›)
          qed
        qed
      qed
    next
      show ‹deadlock_freeSKIPS P ⟷ DFSKIPS α(P) ✓s(P) ⊑F P› if ‹α(P) ≠ {}›
      proof (rule iffI)
        show ‹DFSKIPS α(P) ✓s(P) ⊑F P ⟹ deadlock_freeSKIPS P›
          by (meson DFSKIPS_subset ‹✓s(P) ≠ {}› ‹α(P) ≠ {}›
                    deadlock_freeSKIPS_def leFD_imp_leF subset_UNIV that trans_F)
      next
        have ‹Q ∈ ℛproc P ⟹ DFSKIPS UNIV UNIV ⊑F Q ⟹ DFSKIPS α(P) ✓s(P) ⊑F Q› for Q
        proof (unfold DFSKIPS_def, induct arbitrary: Q rule: cont_parallel_fix_ind)
          show ‹cont (λx. (⊓a ∈ UNIV → x) ⊓ SKIPS UNIV)› by simp
        next
          show ‹cont (λx. (⊓a ∈ α(P) → x) ⊓ SKIPS ✓s(P))› by simp
        next
          show ‹adm (λx. ∀Q. Q ∈ ℛproc P ⟶ fst x ⊑F Q ⟶ snd x ⊑F Q)› by simp
        next
          show ‹⋀Q. ⊥ ⊑F Q› by simp
        next
          fix x y Q assume hyp : ‹Q ∈ ℛproc P ⟹ x ⊑F Q ⟹ y ⊑F Q› for Q
          assume ‹Q ∈ ℛproc P› and ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q›
          consider ‹{a. ev a ∈ Q0} = {}› ‹{r. ✓(r) ∈ Q0} = {}›
            | ‹{a. ev a ∈ Q0} = {}› ‹{r. ✓(r) ∈ Q0} ≠ {}›
            | ‹{a. ev a ∈ Q0} ≠ {}› by blast
            
          thus ‹(⊓a ∈ α(P) → y) ⊓ SKIPS ✓s(P) ⊑F Q›
          proof cases
            assume ‹{a. ev a ∈ Q0} = {}› ‹{r. ✓(r) ∈ Q0} = {}›
            hence ‹Q0 = {}› by (metis Collect_empty_eq all_not_in_conv eventptick.exhaust)
            hence ‹Q = STOP› by (simp add: initials_empty_iff_STOP)
            with ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q› have False
              by (auto simp add: failure_refine_def Process_eq_spec
                                 F_STOP F_Ndet F_Mndetprefix' F_SKIPS)
            thus ‹(⊓a ∈ α(P) → y) ⊓ SKIPS ✓s(P) ⊑F Q› ..
          next
            assume ‹{a. ev a ∈ Q0} = {}› ‹{r. ✓(r) ∈ Q0} ≠ {}›
            have ‹SKIPS {r. ✓(r) ∈ Q0} ⊑F Q›
            proof (unfold failure_refine_def, safe)
              show ‹(t, X) ∈ ℱ (SKIPS {r. ✓(r) ∈ Q0})› if ‹(t, X) ∈ ℱ Q› for t X
              proof (cases t)
                assume ‹t = []›
                with ‹(t, X) ∈ ℱ Q› have ‹([], X ∪ - Q0) ∈ ℱ Q›
                  by (metis ComplD initials_memI is_processT5_S7' self_append_conv2)
                with ‹t = []› ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q› ‹{a. ev a ∈ Q0} = {}›
                show ‹(t, X) ∈ ℱ (SKIPS {r. ✓(r) ∈ Q0})›
                  by (simp add: failure_refine_def F_Ndet F_Mndetprefix' F_SKIPS subset_iff)
                     (metis Compl_iff Un_iff neq_Nil_conv)
              next
                from ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q› ‹{a. ev a ∈ Q0} = {}›
                      ‹(t, X) ∈ ℱ Q› F_T initials_memI
                show ‹t = e # t' ⟹ (t, X) ∈ ℱ (SKIPS {r. ✓(r) ∈ Q0})› for e t'
                  by (simp add: failure_refine_def F_Ndet F_Mndetprefix' F_SKIPS) blast
              qed
            qed
            moreover from ‹Q ∈ ℛproc P› ‹{r. ✓(r) ∈ Q0} ≠ {}› initial_tick_imp_in_ticks_of
                          ticks_of_reachable_processes_subset
            have ‹SKIPS ✓s(P) ⊑F SKIPS {r. ✓(r) ∈ Q0}›
              by (force simp add: SKIPS_F_SKIPS_iff ‹✓s(P) ≠ {}›)
            ultimately show ‹(⊓a ∈ α(P) → y) ⊓ SKIPS ✓s(P) ⊑F Q›
              using Ndet_F_self_right trans_F by blast
          next
            assume ‹{a. ev a ∈ Q0} ≠ {}›
            from ‹Q ∈ ℛproc P› initial_tick_imp_in_ticks_of ticks_of_reachable_processes_subset
            have ‹{r. ✓(r) ∈ Q0} ⊆ ✓s(P)› by force
            from ‹Q ∈ ℛproc P› events_of_reachable_processes_subset initial_ev_imp_in_events_of
            have ‹(⊓a ∈ α(P) → y) ⊓ SKIPS ✓s(P) ⊑F (⊓a ∈ {a. ev a ∈ Q0} → y) ⊓ SKIPS ✓s(P)›
              by (force intro: mono_Ndet_F[OF Mndetprefix_F_subset[OF ‹{a. ev a ∈ Q0} ≠ {}›] idem_F])
            moreover have ‹… ⊑F (⊓a ∈ {a. ev a ∈ Q0} → Q after a) ⊓ SKIPS ✓s(P)›
            proof (rule mono_Ndet_F[OF mono_Mndetprefix_F idem_F], clarify)
              show ‹ev a ∈ Q0 ⟹ y ⊑F Q after a› for a
                by (frule mono_After_F[OF _ ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q›])
                   (simp add: After_Ndet initials_Mndetprefix image_iff
                              After_Mndetprefix reachable_after ‹Q ∈ ℛproc P› hyp)
            qed
            moreover have ‹… ⊑F Q›
            proof (unfold failure_refine_def, safe)
              show ‹(t, X) ∈ ℱ ((⊓a ∈ {a. ev a ∈ Q0} → Q after a) ⊓ SKIPS ✓s(P))› if ‹(t, X) ∈ ℱ Q› for t X
              proof (cases t)
                assume ‹t = []›
                with ‹(t, X) ∈ ℱ Q› have ‹([], X ∪ - Q0) ∈ ℱ Q›
                  by (metis ComplD eq_Nil_appendI initials_memI' is_processT5_S7')
                with ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q› ‹{r. ✓(r) ∈ Q0} ⊆ ✓s(P)›
                show ‹(t, X) ∈ ℱ ((⊓a ∈ {a. ev a ∈ Q0} → Q after a) ⊓ SKIPS ✓s(P))›
                  by (simp add: failure_refine_def F_Ndet F_Mndetprefix' ‹t = []› F_SKIPS ‹✓s(P) ≠ {}› subset_iff)
                     (meson ComplI UnI1 UnI2 list.distinct(1))
              next
                from ‹(t, X) ∈ ℱ Q› ‹(⊓a ∈ UNIV → x) ⊓ SKIPS UNIV ⊑F Q› ‹{r. ✓(r) ∈ Q0} ⊆ ✓s(P)›
                show ‹t = e # t' ⟹ (t, X) ∈ ℱ ((⊓a ∈ {a. ev a ∈ Q0} → Q after a) ⊓ SKIPS ✓s(P))› for e t'
                  by (simp add: failure_refine_def F_Ndet F_Mndetprefix' F_SKIPS F_After ‹✓s(P) ≠ {}› subset_iff)
                     (metis F_T initials_memI list.distinct(1) list.inject)
              qed
            qed
            ultimately show ‹(⊓a ∈ α(P) → y) ⊓ SKIPS ✓s(P) ⊑F Q› using trans_F by blast
          qed
        qed
        thus ‹deadlock_freeSKIPS P ⟹ DFSKIPS α(P) ✓s(P) ⊑F P›
          by (simp add: deadlock_freeSKIPS_def reachable_self)
      qed
    qed
  qed
qed

corollary deadlock_freeSKIPS_iff_DFSKIPS_events_of_ticks_of_leFD :
  ‹deadlock_freeSKIPS P ⟷ (  if α(P) = {} ∧ ✓s(P) = {} then False
                            else   if ✓s(P) = {} then DF α(P) ⊑FD P
                                 else   if α(P) = {} then SKIPS ✓s(P) ⊑FD P
                                      else DFSKIPS α(P) ✓s(P) ⊑FD P)›
  by (metis deadlock_freeSKIPS_iff_DFSKIPS_events_of_ticks_of_leF D_SKIPS deadlock_freeSKIPS_FD
            div_free_DF div_free_DFSKIPS divergence_refine_def failure_divergence_refine_def)

corollary deadlock_freeSKIPS_iff_DFSKIPS_strict_events_of_strict_ticks_of_leF :
  ‹deadlock_freeSKIPS P ⟷ (  if α(P) = {} ∧ ✓s(P) = {} then False
                            else   if ✓s(P) = {} then DF α(P) ⊑F P
                                 else   if α(P) = {} then SKIPS ✓s(P) ⊑F P
                                      else DFSKIPS α(P) ✓s(P) ⊑F P)›
  by (simp add: deadlock_freeSKIPS_iff_DFSKIPS_events_of_ticks_of_leF
                events_of_is_strict_events_of_or_UNIV ticks_of_is_strict_ticks_of_or_UNIV)
     (meson deadlock_free_iff_DF_strict_events_of_leF DFSKIPS_subset deadlock_freeSKIPS_SKIPS
            deadlock_freeSKIPS_def deadlock_freeSKIPS_implies_div_free trans_F
            deadlock_free_implies_div_free failure_divergence_refine_def subset_UNIV)

corollary deadlock_freeSKIPS_iff_DFSKIPS_strict_events_of_strict_ticks_of_leFD :
  ‹deadlock_freeSKIPS P ⟷ (  if α(P) = {} ∧ ✓s(P) = {} then False
                            else   if ✓s(P) = {} then DF α(P) ⊑FD P
                                 else   if α(P) = {} then SKIPS ✓s(P) ⊑FD P
                                      else DFSKIPS α(P) ✓s(P) ⊑FD P)›
  by (metis deadlock_freeSKIPS_iff_DFSKIPS_events_of_ticks_of_leFD
            deadlock_freeSKIPS_iff_DFSKIPS_strict_events_of_strict_ticks_of_leF
            deadlock_freeSKIPS_implies_div_free events_of_is_strict_events_of_or_UNIV
            leFD_imp_leF ticks_of_is_strict_ticks_of_or_UNIV)



subsection ‹Big results›

text ‹As consequences, we have very powerful results,
      and especially a ``data independence'' deadlock freeness theorem.›

lemma deadlock_free_is_right:
  ‹deadlock_free P ⟷ (∀t ∈ 𝒯 P. tF t ∧ (t,      UNIV) ∉ ℱ P)›
  ‹deadlock_free P ⟷ (∀t ∈ 𝒯 P. tF t ∧ (t, ev ` UNIV) ∉ ℱ P)›
proof -
  from  deadlock_free_iff_empty_ticks_of_and_deadlock_freeSKIPS
        deadlock_freeSKIPS_is_right tickFree_traces_iff_empty_ticks_of
  show ‹deadlock_free P ⟷ (∀t ∈ 𝒯 P. tF t ∧ (t, UNIV) ∉ ℱ P)› by blast
  thus ‹deadlock_free P ⟷ (∀t ∈ 𝒯 P. tF t ∧ (t, ev ` UNIV) ∉ ℱ P)›
    by (auto intro: is_processT4)
       (metis Aftertrace.simps(1) deadlock_free_Aftertick_characterization
              F_imp_R_Aftertrace deadlock_free_Aftertrace_characterization)
qed

end

―‹We may probably prove term‹deadlock_free P ⟷ (∀t ∈ 𝒯 P. tF t ∧ (t, ev ` α(P)) ∉ ℱ P)››



theorem data_independence_deadlock_free_Sync:
  fixes P Q :: ‹('a, 'r) processptick›
  assumes df_P : ‹deadlock_free P› and df_Q : ‹deadlock_free Q›
  and hyp : ‹events_of Q ∩ S = {} ∨ (∃y. events_of Q ∩ S = {y} ∧ events_of P ∩ S ⊆ {y})›
shows ‹deadlock_free (P ⟦S⟧ Q)›
proof -
  have non_BOT : ‹P ≠ ⊥› ‹Q ≠ ⊥›
    by (simp_all add: BOT_iff_Nil_D deadlock_free_implies_div_free df_P df_Q)

  have nonempty_events : ‹events_of P ≠ {}› ‹events_of Q ≠ {}›
    by (simp_all add: df_P df_Q nonempty_events_of_if_deadlock_free)
  
  obtain a b where initial : ‹ev a ∈ P0› ‹ev b ∈ Q0›
    by (meson deadlock_free_initial_evE df_P df_Q)

  have ‹ev a ∈ (P ⟦S⟧ Q)0 ∨ ev b ∈ (P ⟦S⟧ Q)0›
    by (simp add: initials_Sync non_BOT image_iff)
       (metis events_of_iff_reachable_ev reachable_ev.intros(1) 
              Int_iff initial empty_iff hyp insert_iff subset_singleton_iff)
  hence nonempty_events_Sync: ‹α(P ⟦S⟧ Q) ≠ {}›
    by (metis events_of_iff_reachable_ev empty_iff reachable_ev.intros(1))

  have * : ‹DF (α(P) ∪ α(Q)) ⊑FD DF α(P) ⟦S⟧ DF α(Q)›
    by (simp add: DF_FD_DF_Sync_DF hyp nonempty_events)

  also have ‹… ⊑FD P ⟦S⟧ Q›
    by (meson deadlock_free_iff_DF_events_of_leFD df_P df_Q mono_Sync_FD)

  ultimately show ‹deadlock_free (P ⟦S⟧ Q)›
    by (meson DF_Univ_freeness Un_empty nonempty_events(1) trans_FD)
qed

lemma data_independence_deadlock_free_Sync_bis:
  ‹⟦deadlock_free P; deadlock_free Q; α(Q) ∩ S = {}⟧ ⟹
   deadlock_free (P ⟦S⟧ Q)› for P :: ‹('a, 'r) processptick›
  by (simp add: data_independence_deadlock_free_Sync)


text ‹We can't expect much better without hypothesis on the processes term‹P› and term‹Q›.
      We can easily build the following counter example.›

lemma ‹∃P Q S. deadlock_free P ∧ deadlock_free Q ∧
               (∃y z. events_of Q ∩ S ⊆ {y, z} ∧ events_of P ∩ S ⊆ {y, z}) ∧
               ¬ deadlock_free (P ⟦S :: nat set⟧ Q)›
proof (intro exI conjI)
  show ‹deadlock_free (DF {0})› and ‹deadlock_free (DF {Suc 0})›
    by (metis DF_Univ_freeness empty_not_insert idem_FD)+
next
  show ‹events_of (DF {Suc 0}) ∩ {0, Suc 0} ⊆ {0, Suc 0}›
   and ‹events_of (DF {0}) ∩ {0, Suc 0} ⊆ {0, Suc 0}› by simp_all
next
  have ‹DF {0} ⟦{0, Suc 0}⟧ DF {Suc 0} = STOP›
    by (simp add: initials_empty_iff_STOP[symmetric]
                  initials_Sync initials_DF BOT_iff_Nil_D div_free_DF)
  from this[THEN arg_cong[where f = deadlock_free]]
  show ‹¬ deadlock_free (DF {0} ⟦{0, Suc 0}⟧ DF {Suc 0})›
    by (simp add: non_deadlock_free_STOP)
qed

end

find_theorems name:  data_independence_deadlock_free_Sync_bis

― ‹Think about a const‹deadlock_freeSKIPS› version.›


subsection ‹Results with other references Processes ›

subsubsection ‹const‹RUN› and const‹non_terminating››

lemma non_terminating_STOP [simp] : ‹non_terminating STOP›
  unfolding non_terminating_def by simp

lemma not_non_terminating_SKIP [simp]: ‹¬ non_terminating (SKIP r)›
  unfolding non_terminating_is_right by (simp add: T_SKIP)

lemma not_non_terminating_BOT [simp] : ‹¬ non_terminating ⊥›
  unfolding non_terminating_is_right T_BOT
  using front_tickFree_single non_tickFree_tick by (metis mem_Collect_eq)


context AfterExt begin

lemma non_terminating_iff_RUN_events_T:
  ‹non_terminating P ⟷ RUN α(P) ⊑T P› for P :: ‹('a, 'r) processptick›
proof (intro iffI)
  have RUN_subset_T: ‹(A :: 'a set) ⊆ B ⟹ RUN B ⊑T RUN A› for A B
    by (drule RUN_subset_DT, unfold trace_divergence_refine_def, elim conjE, assumption)
  show ‹RUN (events_of P) ⊑T P ⟹ non_terminating P›
    unfolding non_terminating_def by (meson RUN_subset_T UNIV_I subsetI trans_T)
next
  assume non_terminating_P: ‹non_terminating P›
  have ‹Q ∈ ℛproc P ⟹ RUN (events_of P) ⊑T Q› for Q
  proof (unfold RUN_def, induct rule: reachable_processes_fix_ind_T)
    show ‹cont (λx. □e ∈ events_of P → x)› by simp
  next
    fix x s
    assume hyp: ‹∀Q ∈ ℛproc P. x ⊑T Q›
    show ‹s ∈ 𝒯 P ⟹ tickFree s ⟹ □e ∈ events_of P → x ⊑T P after𝒯 s›
    proof (unfold trace_refine_def, safe)
      show ‹s ∈ 𝒯 P ⟹ tickFree s ⟹ t ∈ 𝒯 (P after𝒯 s) ⟹
            t ∈ 𝒯 (□e ∈ events_of P → x)› for t
      proof (induct t arbitrary: s)
        show ‹[] ∈ 𝒯 (□e∈events_of P → x)› by simp
      next
        case (Cons e t)
        from Cons.prems(1, 2) have * : ‹P after𝒯 s ∈ ℛproc P›
          by (auto simp add: reachable_processes_is)
        obtain e' where ** : ‹e = ev e'› ‹e' ∈ events_of P›
          by (meson Cons.prems(1, 3) initials_memI imageE
                    non_terminating_P initials_Aftertrace_subset_events_of set_mp)
        from Cons.prems T_Aftertrace "**"(1)
        have ‹t ∈ 𝒯 (P after𝒯 (s @ [e]))› by (simp add: T_Aftertrace_eq)
        also have ‹… ⊆ 𝒯 x›
          apply (rule hyp[rule_format, unfolded trace_refine_def,
                        of ‹P after𝒯 (s @ [e])›, simplified])
          apply (simp add: Aftertrace_snoc "**"(1) Aftertick_def)
          apply (rule reachable_after[OF "*" ])
          using Cons.prems(3) initials_memI F_T "**"(1) by blast
        finally have ‹t ∈ 𝒯 x› .
        with "**" show ?case by (auto simp add: T_Mprefix)
      qed
    qed
  qed
  with reachable_self show ‹RUN α(P) ⊑T P› by blast
qed



lemma lifelock_free_F: ‹lifelock_free P ⟷ CHAOS UNIV ⊑F P›
  by (simp add: lifelock_free_is_non_terminating non_terminating_F)



end 

(*<*)
end
(*>*)