Theory CSP_Monotonies

(*<*)
―‹ ********************************************************************
 * 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       : CSP monotonies
 *
 * 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.
 ******************************************************************************›
(*>*)

section ‹ Monotonies ›

(*<*)
theory CSP_Monotonies 
  imports Constant_Processes Deterministic_Choice Non_Deterministic_Choice
    Global_Non_Deterministic_Choice Sliding_Choice
    Multi_Deterministic_Prefix_Choice Multi_Non_Deterministic_Prefix_Choice
    Sequential_Composition Synchronization_Product Hiding Renaming CSP_Refinements
begin
  (*>*)

subsection ‹Straight Monotony›

subsubsection ‹ Non Deterministic Choice ›

lemma mono_Ndet_FD : ‹P ⊑⇩F⇩D P' ⟹ Q ⊑⇩F⇩D Q' ⟹ P ⊓ Q ⊑⇩F⇩D P' ⊓ Q'›
  and mono_Ndet_DT : ‹P ⊑⇩D⇩T P' ⟹ Q ⊑⇩D⇩T Q' ⟹ P ⊓ Q ⊑⇩D⇩T P' ⊓ Q'›
  and mono_Ndet_F  : ‹P ⊑⇩F P' ⟹ Q ⊑⇩F Q' ⟹ P ⊓ Q ⊑⇩F P' ⊓ Q'›
  and mono_Ndet_D  : ‹P ⊑⇩D P' ⟹ Q ⊑⇩D Q' ⟹ P ⊓ Q ⊑⇩D P' ⊓ Q'›
  and mono_Ndet_T  : ‹P ⊑⇩T P' ⟹ Q ⊑⇩T Q' ⟹ P ⊓ Q ⊑⇩T P' ⊓ Q'›
  by (auto simp add: refine_defs Ndet_projs)

lemmas monos_Ndet = mono_Ndet mono_Ndet_FD mono_Ndet_DT
  mono_Ndet_F mono_Ndet_D mono_Ndet_T



subsubsection ‹ Global Non Deterministic Choice ›

lemma mono_GlobalNdet_FD : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F⇩D Q a) ⟹ (⊓a ∈ A. P a) ⊑⇩F⇩D ⊓a ∈ A. Q a›
  and mono_GlobalNdet_DT : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D⇩T Q a) ⟹ (⊓a ∈ A. P a) ⊑⇩D⇩T ⊓a ∈ A. Q a›
  and mono_GlobalNdet_F  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F Q a) ⟹ (⊓a ∈ A. P a) ⊑⇩F ⊓a ∈ A. Q a›
  and mono_GlobalNdet_D  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D Q a) ⟹ (⊓a ∈ A. P a) ⊑⇩D ⊓a ∈ A. Q a›
  and mono_GlobalNdet_T  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩T Q a) ⟹ (⊓a ∈ A. P a) ⊑⇩T ⊓a ∈ A. Q a›
  by (auto simp add: refine_defs GlobalNdet_projs)

lemmas monos_GlobalNdet = mono_GlobalNdet mono_GlobalNdet_FD mono_GlobalNdet_DT
  mono_GlobalNdet_F mono_GlobalNdet_D mono_GlobalNdet_T


lemma GlobalNdet_FD_subset : ‹A ≠ {} ⟹ A ⊆ B ⟹ (⊓a ∈ B. P a) ⊑⇩F⇩D (⊓a ∈ A. P a)›
  and GlobalNdet_DT_subset : ‹A ⊆ B ⟹ (⊓a ∈ B. P a) ⊑⇩D⇩T (⊓a ∈ A. P a)›
  and GlobalNdet_F_subset  : ‹A ≠ {} ⟹ A ⊆ B ⟹ (⊓a ∈ B. P a) ⊑⇩F (⊓a ∈ A. P a)›  
  and GlobalNdet_T_subset  : ‹A ⊆ B ⟹ (⊓a ∈ B. P a) ⊑⇩T (⊓a ∈ A. P a)›
  and GlobalNdet_D_subset  : ‹A ⊆ B ⟹ (⊓a ∈ B. P a) ⊑⇩D (⊓a ∈ A. P a)›
  by (auto simp add: refine_defs GlobalNdet_projs)

lemmas GlobalNdet_le_subset =
  GlobalNdet_FD_subset GlobalNdet_DT_subset
  GlobalNdet_F_subset GlobalNdet_T_subset GlobalNdet_D_subset



subsubsection ‹ Deterministic Choice ›

lemma mono_Det_FD : ‹P ⊑⇩F⇩D P' ⟹ Q ⊑⇩F⇩D Q' ⟹ P □ Q ⊑⇩F⇩D P' □ Q'›
proof (rule trans_FD)
  show ‹P ⊑⇩F⇩D P' ⟹ P □ Q ⊑⇩F⇩D P' □ Q›
    unfolding refine_defs F_Det D_Det using F_T T_F by blast
next
  show ‹Q ⊑⇩F⇩D Q' ⟹ P' □ Q ⊑⇩F⇩D P' □ Q'›
    unfolding refine_defs F_Det D_Det using F_T T_F by blast
qed

lemma mono_Det_D : ‹P ⊑⇩D P' ⟹ Q ⊑⇩D Q' ⟹ P □ Q ⊑⇩D P' □ Q'›
  by (metis D_Det Un_mono divergence_refine_def)

lemma mono_Det_T : ‹P ⊑⇩T P' ⟹ Q ⊑⇩T Q' ⟹ P □ Q ⊑⇩T P' □ Q'›
  by (metis T_Det Un_mono trace_refine_def)

corollary mono_Det_DT : ‹P ⊑⇩D⇩T P' ⟹ Q ⊑⇩D⇩T Q' ⟹ P □ Q ⊑⇩D⇩T P' □ Q'›
  by (simp_all add: trace_divergence_refine_def mono_Det_D mono_Det_T)

text ‹Deterministic choice monotony doesn't hold for \<^term>‹(⊑⇩F)›.›

lemmas monos_Det = mono_Det mono_Det_FD mono_Det_DT
  mono_Det_D mono_Det_T



subsubsection ‹Sliding choice›

lemma mono_Sliding_FD : ‹P ⊑⇩F⇩D P' ⟹ Q ⊑⇩F⇩D Q' ⟹ P ⊳ Q ⊑⇩F⇩D P' ⊳ Q'›
  and mono_Sliding_DT : ‹P ⊑⇩D⇩T P' ⟹ Q ⊑⇩D⇩T Q' ⟹ P ⊳ Q ⊑⇩D⇩T P' ⊳ Q'›
  and mono_Sliding_D  : ‹P ⊑⇩D P' ⟹ Q ⊑⇩D Q' ⟹ P ⊳ Q ⊑⇩D P' ⊳ Q'›
  and mono_Sliding_T  : ‹P ⊑⇩T P' ⟹ Q ⊑⇩T Q' ⟹ P ⊳ Q ⊑⇩T P' ⊳ Q'›
  unfolding Sliding_def by (simp_all add: monos_Det monos_Ndet)

text ‹Sliding choice monotony doesn't hold for \<^term>‹(⊑⇩F)›.›

lemma mono_Sliding_F_right : ‹Q ⊑⇩F Q' ⟹ P ⊳ Q ⊑⇩F P ⊳ Q'›
  by (auto simp add: failure_refine_def F_Sliding)

lemmas monos_Sliding = mono_Sliding mono_Sliding_FD mono_Sliding_DT
  mono_Sliding_D mono_Sliding_T mono_Sliding_F_right



subsubsection ‹Synchronization›

lemma mono_Sync_FD : ‹⟦P ⊑⇩F⇩D P'; Q ⊑⇩F⇩D Q'⟧ ⟹ P ⟦S⟧ Q ⊑⇩F⇩D P' ⟦S⟧ Q'›
  for P P' Q Q' :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof (rule trans_FD[of _ ‹P' ⟦S⟧ Q›])
  show ‹P ⟦S⟧ Q ⊑⇩F⇩D P' ⟦S⟧ Q› if ‹P ⊑⇩F⇩D P'› for P P' Q :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  proof (rule failure_divergence_refine_optimizedI)
    from le_ref1 le_ref2T ‹P ⊑⇩F⇩D P'›
    show ‹s ∈ 𝒟 (P' ⟦S⟧ Q) ⟹ s ∈ 𝒟 (P ⟦S⟧ Q)› for s
      unfolding D_Sync by blast
  next
    assume subset_div : ‹𝒟 (P' ⟦S⟧ Q) ⊆ 𝒟 (P ⟦S⟧ Q)›
    fix s Z assume ‹(s, Z) ∈ ℱ (P' ⟦S⟧ Q)›
    then consider ‹s ∈ 𝒟 (P' ⟦S⟧ Q)›
      | (F) t u X Y where ‹(t, X) ∈ ℱ P'› ‹(u, Y) ∈ ℱ Q›
        ‹s setinterleaves ((t, u), range tick ∪ ev ` S)›
        ‹Z = (X ∪ Y) ∩ (range tick ∪ ev ` S) ∪ X ∩ Y›
      unfolding F_Sync D_Sync by blast
    thus ‹(s, Z) ∈ ℱ (P ⟦S⟧ Q)›
    proof cases
      from subset_div D_F show ‹s ∈ 𝒟 (P' ⟦S⟧ Q) ⟹ (s, Z) ∈ ℱ (P ⟦S⟧ Q)› by blast
    next
      case F
      with le_ref2[OF ‹P ⊑⇩F⇩D P'›] show ‹(s, Z) ∈ ℱ (P ⟦S⟧ Q)› unfolding F_Sync by blast
    qed
  qed
  thus ‹Q ⊑⇩F⇩D Q' ⟹ P' ⟦S⟧ Q ⊑⇩F⇩D P' ⟦S⟧ Q'› by (metis Sync_commute)
qed

lemma mono_Sync_DT : ‹P ⊑⇩D⇩T P' ⟹ Q ⊑⇩D⇩T Q' ⟹ P ⟦S⟧ Q ⊑⇩D⇩T P' ⟦S⟧ Q'›
  by (simp add: refine_defs T_Sync D_Sync) blast


lemmas mono_Par = mono_Sync[where A = UNIV]
  and mono_Par_FD = mono_Sync_FD[where S = UNIV]
  and mono_Par_DT = mono_Sync_DT[where S = UNIV]
  and mono_Inter = mono_Sync[where A = ‹{}›]
  and mono_Inter_FD = mono_Sync_FD[where S = ‹{}›]
  and mono_Inter_DT = mono_Sync_DT[where S = ‹{}›]


lemmas monos_Sync = mono_Sync mono_Sync_FD mono_Sync_DT
  and monos_Par = mono_Par mono_Par_FD mono_Par_DT
  and monos_Inter = mono_Inter mono_Inter_FD mono_Inter_DT



subsubsection ‹Sequential composition›

lemma mono_Seq_FD : ‹P ⊑⇩F⇩D P' ⟹ Q ⊑⇩F⇩D Q' ⟹ P ❙; Q ⊑⇩F⇩D P' ❙; Q'›
  by (simp add: refine_defs Seq_projs subset_iff) (metis T_F_spec)

lemma mono_Seq_DT : ‹P ⊑⇩D⇩T P' ⟹ Q ⊑⇩D⇩T Q' ⟹ P ❙; Q ⊑⇩D⇩T P' ❙; Q'›
  by (simp add: refine_defs Seq_projs subset_iff) blast

lemma mono_Seq_F_right : ‹Q ⊑⇩F Q' ⟹ P ❙; Q ⊑⇩F P ❙; Q'›
  by (simp add: failure_refine_def F_Seq) blast

lemma mono_Seq_D_right : ‹Q ⊑⇩D Q' ⟹ P ❙; Q ⊑⇩D P ❙; Q'›
  by (simp add: divergence_refine_def D_Seq) blast

lemma mono_Seq_T_right : ‹Q ⊑⇩T Q' ⟹ P ❙; Q ⊑⇩T P ❙; Q'›
  by (simp add: trace_refine_def T_Seq) blast

text ‹Left Sequence monotony doesn't hold for \<^term>‹(⊑⇩F)›, \<^term>‹(⊑⇩D)› and \<^term>‹(⊑⇩T)›.›

lemmas monos_Seq = mono_Seq mono_Seq_FD mono_Seq_DT
  mono_Seq_F_right mono_Seq_D_right mono_Seq_T_right



subsubsection ‹Renaming›

lemma mono_Renaming_D : ‹P ⊑⇩D Q ⟹ Renaming P f g ⊑⇩D Renaming Q f g›
  unfolding divergence_refine_def D_Renaming by blast

lemma mono_Renaming_FD : ‹P ⊑⇩F⇩D Q ⟹ Renaming P f g ⊑⇩F⇩D Renaming Q f g›
  using mono_Renaming_D unfolding refine_defs F_Renaming D_Renaming by blast

lemma mono_Renaming_DT : ‹P ⊑⇩D⇩T Q ⟹ Renaming P f g ⊑⇩D⇩T Renaming Q f g›
  using mono_Renaming_D unfolding refine_defs T_Renaming D_Renaming by blast

lemmas monos_Renaming = mono_Renaming mono_Renaming_FD mono_Renaming_DT mono_Renaming_D



subsubsection ‹Hiding›

lemma mono_Hiding_leT_imp_leD : ‹P \ A ⊑⇩D Q \ A› if ‹A ≠ {}› and ‹P ⊑⇩T Q›
proof (unfold divergence_refine_def, rule subsetI)
  fix s assume ‹s ∈ 𝒟 (Q \ A)›
  then obtain t u
    where * : ‹front_tickFree u› ‹tickFree t›
      ‹s = trace_hide t (ev ` A) @ u›
      ‹t ∈ 𝒟 Q ∨ (∃x. isInfHidden_seqRun x Q A t)›
    unfolding D_Hiding_seqRun by blast
  from "*"(4) have ‹∃x. isInfHidden_seqRun x P A t›
  proof (elim disjE exE)
    assume ‹t ∈ 𝒟 Q›
    from ‹A ≠ {}› obtain a where ‹a ∈ A› by blast
    have ‹isInfHidden_seqRun (λi. ev a) P A t›
    proof (intro allI conjI)
      have ‹seqRun t (λi. ev a) i ∈ 𝒟 Q› for i
        by (induct i) (simp_all add: ‹t ∈ 𝒟 Q› is_processT7 tickFree_seqRun_iff "*"(2))
      thus ‹seqRun t (λi. ev a) i ∈ 𝒯 P› for i
        by (meson D_T ‹P ⊑⇩T Q› trace_refine_def subset_iff)
    next
      from ‹a ∈ A› show ‹ev a ∈ ev ` A› by simp
    qed
    thus ‹∃x. isInfHidden_seqRun x P A t› by blast
  next
    show ‹isInfHidden_seqRun x Q A t ⟹ ∃x. isInfHidden_seqRun x P A t› for x
      by (meson ‹P ⊑⇩T Q› trace_refine_def subset_iff)
  qed
  with "*"(1, 2, 3) show ‹s ∈ 𝒟 (P \ A)› unfolding D_Hiding_seqRun by blast
qed


lemma mono_Hiding_F : ‹P \ A ⊑⇩F Q \ A› if ‹P ⊑⇩F Q›
proof (cases ‹A = {}›)
  from ‹P ⊑⇩F Q› show ‹A = {} ⟹ P \ A ⊑⇩F Q \ A›
    by (auto simp add: failure_refine_def F_Hiding_seqRun subset_iff
        intro: is_processT7 is_processT8)
next
  show ‹P \ A ⊑⇩F Q \ A› if ‹A ≠ {}›
  proof (unfold failure_refine_def, safe)
    fix s X assume ‹(s, X) ∈ ℱ (Q \ A)›
    then consider ‹s ∈ 𝒟 (Q \ A)›
      | t where ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ ℱ Q›
      unfolding F_Hiding_seqRun D_Hiding_seqRun by blast
    thus ‹(s, X) ∈ ℱ (P \ A)›
    proof cases
      fix t assume ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ ℱ Q›
      from ‹P ⊑⇩F Q› ‹(t, X ∪ ev ` A) ∈ ℱ Q› have ‹(t, X ∪ ev ` A) ∈ ℱ P›
        unfolding failure_refine_def by blast
      with ‹s = trace_hide t (ev ` A)› show ‹(s, X) ∈ ℱ (P \ A)›
        unfolding F_Hiding by blast
    next
      from mono_Hiding_leT_imp_leD[OF ‹A ≠ {}› ‹P ⊑⇩F Q›[THEN leF_imp_leT]]
      show ‹s ∈ 𝒟 (Q \ A) ⟹ (s, X) ∈ ℱ (P \ A)›
        by (simp add: divergence_refine_def in_mono is_processT8)
    qed
  qed
qed

lemma mono_Hiding_T : ‹P \ A ⊑⇩T Q \ A› if ‹P ⊑⇩T Q›
proof (cases ‹A = {}›)
  from ‹P ⊑⇩T Q› show ‹A = {} ⟹ P \ A ⊑⇩T Q \ A›
    by (auto simp add: trace_refine_def T_Hiding_seqRun
        subset_iff F_T T_F D_T is_processT7)
next
  show ‹P \ A ⊑⇩T Q \ A› if ‹A ≠ {}›
  proof (unfold trace_refine_def, rule subsetI)
    fix s assume ‹s ∈ 𝒯 (Q \ A)›
    then consider ‹s ∈ 𝒟 (Q \ A)›
      | t where ‹s = trace_hide t (ev ` A)› ‹(t, ev ` A) ∈ ℱ Q›
      unfolding T_Hiding_seqRun D_Hiding_seqRun by blast
    thus ‹s ∈ 𝒯 (P \ A)›
    proof cases
      fix t assume ‹s = trace_hide t (ev ` A)› ‹(t, ev ` A) ∈ ℱ Q›
      from ‹(t, ev ` A) ∈ ℱ Q› have ‹t ∈ 𝒯 P›
        by (meson F_T ‹P ⊑⇩T Q› in_mono trace_refine_def)
      with inf_hidden consider 
        t' where ‹trace_hide t' (ev ` A) = trace_hide t (ev ` A)› ‹(t', ev ` A) ∈ ℱ P›
      | f where ‹isInfHiddenRun f P A ∧ t ∈ range f› by blast
      thus ‹s ∈ 𝒯 (P \ A)›
      proof cases
        show ‹trace_hide t' (ev ` A) = trace_hide t (ev ` A) ⟹
              (t', ev ` A) ∈ ℱ P ⟹ s ∈ 𝒯 (P \ A)› for t'
          by (simp add: T_Hiding_seqRun) (metis ‹s = trace_hide t (ev ` A)›)
      next
        show ‹isInfHiddenRun f P A ∧ t ∈ range f ⟹ s ∈ 𝒯 (P \ A)› for f
          by (simp add: T_Hiding)
            (metis T_nonTickFree_imp_decomp ‹s = trace_hide t (ev ` A)›
              ‹t ∈ 𝒯 P› append_self_conv front_tickFree_Nil tick_T_F)
      qed
    next
      from mono_Hiding_leT_imp_leD[OF ‹A ≠ {}› ‹P ⊑⇩T Q›]
      show ‹s ∈ 𝒟 (Q \ A) ⟹ s ∈ 𝒯 (P \ A)›
        by (simp add: divergence_refine_def in_mono D_T)
    qed
  qed
qed

lemma mono_Hiding_FD : ‹P \ A ⊑⇩F⇩D Q \ A› if ‹P ⊑⇩F⇩D Q›
proof (cases ‹A = {}›)
  from ‹P ⊑⇩F⇩D Q› show ‹A = {} ⟹ P \ A ⊑⇩F⇩D Q \ A›
    by (simp add: refine_defs F_Hiding_seqRun D_Hiding_seqRun) blast
next
  show ‹A ≠ {} ⟹ P \ A ⊑⇩F⇩D Q \ A›
    by (unfold failure_divergence_refine_def)
      (simp add: ‹P ⊑⇩F⇩D Q› leFD_imp_leF mono_Hiding_F leF_imp_leT mono_Hiding_leT_imp_leD)
qed

lemma mono_Hiding_DT : ‹P \ A ⊑⇩D⇩T Q \ A› if ‹P ⊑⇩D⇩T Q›
proof (cases ‹A = {}›)
  from ‹P ⊑⇩D⇩T Q› show ‹A = {} ⟹ P \ A ⊑⇩D⇩TQ \ A›
    by (auto simp add: refine_defs T_Hiding_seqRun D_Hiding_seqRun F_T T_F in_mono)
next
  show ‹A ≠ {} ⟹ P \ A ⊑⇩D⇩T Q \ A›
    by (unfold trace_divergence_refine_def)
      (simp add: ‹P ⊑⇩D⇩T Q› leDT_imp_leT mono_Hiding_T mono_Hiding_leT_imp_leD)
qed

text ‹Obviously, Hide monotony doesn't hold for \<^term>‹(⊑⇩D)›.›


lemmas monos_Hiding = mono_Hiding mono_Hiding_FD mono_Hiding_DT
  mono_Hiding_F mono_Hiding_T



subsubsection ‹Prefixes›

lemma mono_Mprefix_FD : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F⇩D Q a) ⟹ Mprefix A P ⊑⇩F⇩D Mprefix A Q›
  and mono_Mprefix_DT : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D⇩T Q a) ⟹ Mprefix A P ⊑⇩D⇩T Mprefix A Q›
  and mono_Mprefix_F  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F Q a) ⟹ Mprefix A P ⊑⇩F Mprefix A Q›
  and mono_Mprefix_T  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩T Q a) ⟹ Mprefix A P ⊑⇩T Mprefix A Q›
  and mono_Mprefix_D  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D Q a) ⟹ Mprefix A P ⊑⇩D Mprefix A Q›
  by (simp add: refine_defs Mprefix_projs, blast)+

lemmas monos_Mprefix = mono_Mprefix mono_Mprefix_FD mono_Mprefix_DT
  mono_Mprefix_F mono_Mprefix_T mono_Mprefix_D

corollary mono_write0_FD : ‹P ⊑⇩F⇩D Q ⟹ (a → P) ⊑⇩F⇩D (a → Q)›
  and     mono_write0_DT : ‹P ⊑⇩D⇩T Q ⟹ (a → P) ⊑⇩D⇩T (a → Q)›
  and     mono_write0_F  : ‹P ⊑⇩F Q ⟹ (a → P) ⊑⇩F (a → Q)›
  and     mono_write0_T  : ‹P ⊑⇩T Q ⟹ (a → P) ⊑⇩T (a → Q)›
  and     mono_write0_D  : ‹P ⊑⇩D Q ⟹ (a → P) ⊑⇩D (a → Q)›
  unfolding write0_def by (simp_all add: monos_Mprefix)

lemmas monos_write0 = mono_write0 mono_write0_FD mono_write0_DT
  mono_write0_F mono_write0_T mono_write0_D


corollary mono_write_FD : ‹P ⊑⇩F⇩D Q ⟹ (c❙!a → P) ⊑⇩F⇩D (c❙!a → Q)›
  and     mono_write_DT : ‹P ⊑⇩D⇩T Q ⟹ (c❙!a → P) ⊑⇩D⇩T (c❙!a → Q)›
  and     mono_write_F  : ‹P ⊑⇩F Q ⟹ (c❙!a → P) ⊑⇩F (c❙!a → Q)›
  and     mono_write_T  : ‹P ⊑⇩T Q ⟹ (c❙!a → P) ⊑⇩T (c❙!a → Q)›
  and     mono_write_D  : ‹P ⊑⇩D Q ⟹ (c❙!a → P) ⊑⇩D (c❙!a → Q)›
  by (simp_all add: write_is_write0 monos_write0)

lemmas monos_write = mono_write mono_write_FD mono_write_DT
  mono_write_F mono_write_T mono_write_D


corollary mono_read_FD : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F⇩D Q a) ⟹ (c❙?a∈A → P a) ⊑⇩F⇩D (c❙?a∈A → Q a)›
  and     mono_read_DT : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D⇩T Q a) ⟹ (c❙?a∈A → P a) ⊑⇩D⇩T (c❙?a∈A → Q a)›
  and     mono_read_F  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F Q a) ⟹ (c❙?a∈A → P a) ⊑⇩F (c❙?a∈A → Q a)›
  and     mono_read_T  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩T Q a) ⟹ (c❙?a∈A → P a) ⊑⇩T (c❙?a∈A → Q a)›
  and     mono_read_D  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D Q a) ⟹ (c❙?a∈A → P a) ⊑⇩D (c❙?a∈A → Q a)›
  unfolding read_def by (simp_all add: monos_Mprefix inv_into_into)

lemmas monos_read = mono_read mono_read_FD mono_read_DT
  mono_read_F mono_read_T mono_read_D


lemma mono_Mndetprefix_FD : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F⇩D Q a) ⟹ Mndetprefix A P ⊑⇩F⇩D Mndetprefix A Q›
  and mono_Mndetprefix_DT : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D⇩T Q a) ⟹ Mndetprefix A P ⊑⇩D⇩T Mndetprefix A Q›
  and mono_Mndetprefix_F  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F Q a) ⟹ Mndetprefix A P ⊑⇩F Mndetprefix A Q›
  and mono_Mndetprefix_T  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩T Q a) ⟹ Mndetprefix A P ⊑⇩T Mndetprefix A Q›
  and mono_Mndetprefix_D  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D Q a) ⟹ Mndetprefix A P ⊑⇩D Mndetprefix A Q›
  by (simp add: refine_defs Mndetprefix_projs, blast)+

lemmas monos_Mndetprefix = mono_Mndetprefix mono_Mndetprefix_FD mono_Mndetprefix_DT
  mono_Mndetprefix_F mono_Mndetprefix_T mono_Mndetprefix_D


corollary mono_ndet_write_FD : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F⇩D Q a) ⟹ (c❙!❙!a∈A → P a) ⊑⇩F⇩D (c❙!❙!a∈A → Q a)›
  and     mono_ndet_write_DT : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D⇩T Q a) ⟹ (c❙!❙!a∈A → P a) ⊑⇩D⇩T (c❙!❙!a∈A → Q a)›
  and     mono_ndet_write_F  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F Q a) ⟹ (c❙!❙!a∈A → P a) ⊑⇩F (c❙!❙!a∈A → Q a)›
  and     mono_ndet_write_T  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩T Q a) ⟹ (c❙!❙!a∈A → P a) ⊑⇩T (c❙!❙!a∈A → Q a)›
  and     mono_ndet_write_D  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D Q a) ⟹ (c❙!❙!a∈A → P a) ⊑⇩D (c❙!❙!a∈A → Q a)›
  unfolding ndet_write_def by (simp_all add: monos_Mndetprefix inv_into_into)

lemmas monos_ndet_write = mono_ndet_write mono_ndet_write_FD mono_ndet_write_DT
  mono_ndet_write_F mono_ndet_write_T mono_ndet_write_D


lemma Mndetprefix_FD_Mprefix : ‹Mndetprefix A P ⊑⇩F⇩D Mprefix A P›
  and Mndetprefix_DT_Mprefix : ‹Mndetprefix A P ⊑⇩D⇩T Mprefix A P›
  and Mndetprefix_F_Mprefix  : ‹Mndetprefix A P ⊑⇩F Mprefix A P›
  and Mndetprefix_T_Mprefix  : ‹Mndetprefix A P ⊑⇩T Mprefix A P›
  and Mndetprefix_D_Mprefix  : ‹Mndetprefix A P ⊑⇩D Mprefix A P›
  by (simp_all add: refine_defs Mprefix_projs Mndetprefix_projs) blast+

lemmas Mndetprefix_le_Mprefix =
  Mndetprefix_FD_Mprefix Mndetprefix_DT_Mprefix
  Mndetprefix_F_Mprefix Mndetprefix_T_Mprefix Mndetprefix_D_Mprefix


corollary ndet_write_FD_read : ‹ndet_write c A P ⊑⇩F⇩D read c A P›
  and     ndet_write_DT_read : ‹ndet_write c A P ⊑⇩D⇩T read c A P›
  and     ndet_write_F_read  : ‹ndet_write c A P ⊑⇩F read c A P›
  and     ndet_write_T_read  : ‹ndet_write c A P ⊑⇩T read c A P›
  and     ndet_write_D_read  : ‹ndet_write c A P ⊑⇩D read c A P›
  by (simp_all add: read_def ndet_write_def Mndetprefix_le_Mprefix)

lemmas ndet_write_le_read =
  ndet_write_FD_read ndet_write_DT_read
  ndet_write_F_read ndet_write_T_read ndet_write_D_read


lemma Mndetprefix_FD_subset : ‹A ≠ {} ⟹ A ⊆ B ⟹ Mndetprefix B P ⊑⇩F⇩D Mndetprefix A P›
  and Mndetprefix_DT_subset : ‹A ⊆ B ⟹ Mndetprefix B P ⊑⇩D⇩T Mndetprefix A P›
  and Mndetprefix_F_subset  : ‹A ≠ {} ⟹ A ⊆ B ⟹ Mndetprefix B P ⊑⇩F Mndetprefix A P›  
  and Mndetprefix_T_subset  : ‹A ⊆ B ⟹ Mndetprefix B P ⊑⇩T Mndetprefix A P›
  and Mndetprefix_D_subset  : ‹A ⊆ B ⟹ Mndetprefix B P ⊑⇩D Mndetprefix A P›
  by (auto simp add: refine_defs Mndetprefix_projs)

lemmas Mndetprefix_le_subset =
  Mndetprefix_FD_subset Mndetprefix_DT_subset
  Mndetprefix_F_subset Mndetprefix_T_subset Mndetprefix_D_subset


lemma ndet_write_FD_subset : ‹A ≠ {} ⟹ (c❙!❙!b∈B → P b) ⊑⇩F⇩D (c❙!❙!a∈A → P a)›
  and ndet_write_DT_subset : ‹(c❙!❙!b∈B → P b) ⊑⇩D⇩T (c❙!❙!a∈A → P a)›
  and ndet_write_F_subset  : ‹A ≠ {} ⟹ (c❙!❙!b∈B → P b) ⊑⇩F (c❙!❙!a∈A → P a)›
  and ndet_write_T_subset  : ‹(c❙!❙!b∈B → P b) ⊑⇩T (c❙!❙!a∈A → P a)›
  and ndet_write_D_subset  : ‹(c❙!❙!b∈B → P b) ⊑⇩D (c❙!❙!a∈A → P a)›
  if ‹inj_on c B› and ‹A ⊆ B›
proof -
  have * : ‹(P ∘ inv_into B c) x = (P ∘ inv_into A c) x› if ‹x ∈ c ` A› for x
  proof -
    from ‹x ∈ c ` A› obtain a where ‹a ∈ A› ‹x = c a› by blast
    from ‹a ∈ A› ‹A ⊆ B› have ‹a ∈ B› by blast
    from ‹A ⊆ B› ‹inj_on c B› inj_on_subset have ‹inj_on c A› by blast
    from ‹a ∈ A› ‹x = c a› ‹inj_on c A› have ‹(inv_into A c) x = a› by simp
    moreover from ‹a ∈ B› ‹x = c a› ‹inj_on c B› have ‹(inv_into B c) x = a› by simp
    ultimately show ‹(P ∘ inv_into B c) x = (P ∘ inv_into A c) x› by simp
  qed
  show ‹A ≠ {} ⟹ (c❙!❙!b∈B → P b) ⊑⇩F⇩D (c❙!❙!a∈A → P a)›
    by (metis ‹A ⊆ B› "*" Mndetprefix_FD_subset empty_is_image
        image_mono mono_Mndetprefix_eq ndet_write_def)
  show ‹(c❙!❙!b∈B → P b) ⊑⇩D⇩T (c❙!❙!a∈A → P a)›
    by (metis ‹A ⊆ B› "*" Mndetprefix_DT_subset
        image_mono mono_Mndetprefix_eq ndet_write_def)
  show ‹A ≠ {} ⟹ (c❙!❙!b∈B → P b) ⊑⇩F (c❙!❙!a∈A → P a)›
    by (metis ‹A ⊆ B› "*" Mndetprefix_F_subset empty_is_image
        image_mono mono_Mndetprefix_eq ndet_write_def)
  show ‹(c❙!❙!b∈B → P b) ⊑⇩T (c❙!❙!a∈A → P a)›
    by (metis ‹A ⊆ B› "*" Mndetprefix_T_subset
        image_mono mono_Mndetprefix_eq ndet_write_def)
  show ‹(c❙!❙!b∈B → P b) ⊑⇩D (c❙!❙!a∈A → P a)›
    by (metis ‹A ⊆ B› "*" Mndetprefix_D_subset
        image_mono mono_Mndetprefix_eq ndet_write_def)
qed

lemmas ndet_write_le_subset =
  ndet_write_FD_subset ndet_write_DT_subset
  ndet_write_F_subset ndet_write_T_subset ndet_write_D_subset


lemma Mndetprefix_FD_write0 : ‹Mndetprefix A P ⊑⇩F⇩D (a → P a)›
  and Mndetprefix_DT_write0 : ‹Mndetprefix A P ⊑⇩D⇩T (a → P a)›
  and Mndetprefix_F_write0  : ‹Mndetprefix A P ⊑⇩F (a → P a)›
  and Mndetprefix_T_write0  : ‹Mndetprefix A P ⊑⇩T (a → P a)›
  and Mndetprefix_D_write0  : ‹Mndetprefix A P ⊑⇩D (a → P a)› if ‹a ∈ A›
  by (rule Mndetprefix_le_subset[of ‹{a}›, simplified, OF ‹a ∈ A›])+

lemmas Mndetprefix_le_write0 =
  Mndetprefix_FD_write0 Mndetprefix_DT_write0
  Mndetprefix_F_write0 Mndetprefix_T_write0 Mndetprefix_D_write0


lemma Mprefix_DT_subset : ‹A ⊆ B ⟹ Mprefix B P ⊑⇩D⇩T Mprefix A P›
  and Mprefix_T_subset  : ‹A ⊆ B ⟹ Mprefix B P ⊑⇩T Mprefix A P›
  and Mprefix_D_subset  : ‹A ⊆ B ⟹ Mprefix B P ⊑⇩D Mprefix A P›
  by (auto simp add: refine_defs Mprefix_projs)

lemmas Mprefix_le_subset = Mprefix_DT_subset Mprefix_T_subset Mprefix_D_subset

text ‹Mprefix set monotony doesn't hold for \<^term>‹(⊑⇩F)› and \<^term>‹(⊑⇩F⇩D)›
      where it holds for deterministic choice.›


lemma read_DT_subset : ‹(c❙?b∈B → P b) ⊑⇩D⇩T (c❙?a∈A → P a)›
  and read_T_subset  : ‹(c❙?b∈B → P b) ⊑⇩T (c❙?a∈A → P a)›
  and read_D_subset  : ‹(c❙?b∈B → P b) ⊑⇩D (c❙?a∈A → P a)›
  if ‹inj_on c B› and ‹A ⊆ B›
proof -
  have * : ‹(P ∘ inv_into B c) x = (P ∘ inv_into A c) x› if ‹x ∈ c ` A› for x
  proof -
    from ‹x ∈ c ` A› obtain a where ‹a ∈ A› ‹x = c a› by blast
    from ‹a ∈ A› ‹A ⊆ B› have ‹a ∈ B› by blast
    from ‹A ⊆ B› ‹inj_on c B› inj_on_subset have ‹inj_on c A› by blast
    from ‹a ∈ A› ‹x = c a› ‹inj_on c A› have ‹(inv_into A c) x = a› by simp
    moreover from ‹a ∈ B› ‹x = c a› ‹inj_on c B› have ‹(inv_into B c) x = a› by simp
    ultimately show ‹(P ∘ inv_into B c) x = (P ∘ inv_into A c) x› by simp
  qed
  show ‹(c❙?b∈B → P b) ⊑⇩D⇩T (c❙?a∈A → P a)›
    by (metis ‹A ⊆ B› "*" Mprefix_DT_subset image_mono mono_Mprefix_eq read_def)
  show ‹(c❙?b∈B → P b) ⊑⇩T (c❙?a∈A → P a)›
    by (metis ‹A ⊆ B› "*" Mprefix_T_subset image_mono mono_Mprefix_eq read_def)
  show ‹(c❙?b∈B → P b) ⊑⇩D (c❙?a∈A → P a)›
    by (metis ‹A ⊆ B› "*" Mprefix_D_subset image_mono mono_Mprefix_eq read_def)
qed



subsection ‹Monotony Properties›

subsubsection ‹ Non Deterministic Choice Operator Laws ›

lemma Ndet_FD_self_left   : ‹P ⊓ Q ⊑⇩F⇩D P›
  and Ndet_DT_self_left   : ‹P ⊓ Q ⊑⇩D⇩T P›
  and Ndet_F_self_left    : ‹P ⊓ Q ⊑⇩F P›
  and Ndet_T_self_left    : ‹P ⊓ Q ⊑⇩T P›
  and Ndet_D_self_left    : ‹P ⊓ Q ⊑⇩D P›
  and Ndet_FD_self_right  : ‹P ⊓ Q ⊑⇩F⇩D Q›
  and Ndet_DT_self_right  : ‹P ⊓ Q ⊑⇩D⇩T Q›
  and Ndet_F_self_right   : ‹P ⊓ Q ⊑⇩F Q›
  and Ndet_T_self_right   : ‹P ⊓ Q ⊑⇩T Q›
  and Ndet_D_self_right   : ‹P ⊓ Q ⊑⇩D Q›
  by (simp_all add: refine_defs Ndet_projs)

lemmas Ndet_le_self_left  = Ndet_FD_self_left Ndet_DT_self_left
  Ndet_F_self_left Ndet_T_self_left Ndet_D_self_left
  and Ndet_le_self_right = Ndet_FD_self_right Ndet_DT_self_right
  Ndet_F_self_right Ndet_T_self_right Ndet_D_self_right

lemma Ndet_FD_Det : ‹P ⊓ Q ⊑⇩F⇩D P □ Q›
  and Ndet_DT_Det : ‹P ⊓ Q ⊑⇩D⇩T P □ Q›
  and Ndet_F_Det  : ‹P ⊓ Q ⊑⇩F P □ Q›
  and Ndet_T_Det  : ‹P ⊓ Q ⊑⇩T P □ Q›
  and Ndet_D_Det  : ‹P ⊓ Q ⊑⇩D P □ Q›
  by (auto simp add: refine_defs Det_projs Ndet_projs
      intro: is_processT8 is_processT6_TR_notin)

lemmas Ndet_le_Det = Ndet_FD_Det Ndet_DT_Det Ndet_F_Det Ndet_T_Det Ndet_D_Det

lemma Ndet_FD_Sliding : ‹P ⊓ Q ⊑⇩F⇩D P ⊳ Q›
  and Ndet_DT_Sliding : ‹P ⊓ Q ⊑⇩D⇩T P ⊳ Q›
  and Ndet_F_Sliding  : ‹P ⊓ Q ⊑⇩F P ⊳ Q›
  and Ndet_T_Sliding  : ‹P ⊓ Q ⊑⇩T P ⊳ Q›
  and Ndet_D_Sliding  : ‹P ⊓ Q ⊑⇩D P ⊳ Q›
  by (auto simp add: refine_defs Ndet_projs Sliding_projs
      intro: is_processT8 is_processT6_TR_notin)

lemmas Ndet_le_Sliding = Ndet_FD_Sliding Ndet_DT_Sliding
  Ndet_F_Sliding Ndet_T_Sliding Ndet_D_Sliding



lemma GlobalNdet_refine_FD : ‹a ∈ A ⟹ ⊓a ∈ A. P a ⊑⇩F⇩D P a›
  using GlobalNdet_FD_subset[of ‹{a}› A] by simp

lemma GlobalNdet_refine_DT : ‹a ∈ A ⟹ ⊓a ∈ A. P a ⊑⇩D⇩T P a›
  using GlobalNdet_DT_subset[of ‹{a}› A] by simp

lemma GlobalNdet_refine_F : ‹a ∈ A ⟹ ⊓a ∈ A. P a ⊑⇩F P a›
  by (simp add: GlobalNdet_refine_FD leFD_imp_leF)

lemma GlobalNdet_refine_D : ‹a ∈ A ⟹ ⊓a ∈ A. P a ⊑⇩D P a›
  by (simp add: GlobalNdet_refine_DT leDT_imp_leD)

lemma GlobalNdet_refine_T : ‹a ∈ A ⟹ ⊓a ∈ A. P a ⊑⇩T P a›
  by (simp add: GlobalNdet_refine_DT leDT_imp_leT)

lemmas GlobalNdet_refine_le = GlobalNdet_refine_FD GlobalNdet_refine_DT
  GlobalNdet_refine_F GlobalNdet_refine_D GlobalNdet_refine_T 


lemma mono_GlobalNdet_FD_const:
  ‹A ≠ {} ⟹ (⋀a. a ∈ A ⟹ P ⊑⇩F⇩D Q a) ⟹ P ⊑⇩F⇩D ⊓a ∈ A. Q a›
  by (metis GlobalNdet_id mono_GlobalNdet_FD)

lemma mono_GlobalNdet_DT_const:
  ‹A ≠ {} ⟹ (⋀a. a ∈ A ⟹ P ⊑⇩D⇩T Q a) ⟹ P ⊑⇩D⇩T ⊓a ∈ A. Q a›
  by (metis GlobalNdet_id mono_GlobalNdet_DT)

lemma mono_GlobalNdet_F_const:
  ‹A ≠ {} ⟹ (⋀a. a ∈ A ⟹ P ⊑⇩F Q a) ⟹ P ⊑⇩F ⊓a ∈ A. Q a›
  by (metis GlobalNdet_id mono_GlobalNdet_F)

lemma mono_GlobalNdet_D_const:
  ‹A ≠ {} ⟹ (⋀a. a ∈ A ⟹ P ⊑⇩D Q a) ⟹ P ⊑⇩D ⊓a ∈ A. Q a›
  by (metis GlobalNdet_id mono_GlobalNdet_D)

lemma mono_GlobalNdet_T_const:
  ‹A ≠ {} ⟹ (⋀a. a ∈ A ⟹ P ⊑⇩T Q a) ⟹ P ⊑⇩T ⊓a ∈ A. Q a›
  by (metis GlobalNdet_id mono_GlobalNdet_T)

lemmas mono_GlobalNdet_le_const = mono_GlobalNdet_FD_const mono_GlobalNdet_DT_const
  mono_GlobalNdet_F_const mono_GlobalNdet_D_const mono_GlobalNdet_T_const



subsubsection ‹ Refinements and Constant Processes ›

lemma STOP_T_iff: ‹STOP ⊑⇩T P ⟷ P = STOP›
  by (metis STOP_iff_T insert_absorb is_processT1_TR subset_singleton_iff trace_refine_def)

lemma STOP_F_iff: ‹STOP ⊑⇩F P ⟷ P = STOP›
  using STOP_T_iff idem_F leF_imp_leT by blast

lemma STOP_FD_iff: ‹STOP ⊑⇩F⇩D P ⟷ P = STOP›
  using STOP_F_iff leFD_imp_leF by blast

lemma STOP_DT_iff: ‹STOP ⊑⇩D⇩T P ⟷ P = STOP›
  using STOP_T_iff idem_DT leDT_imp_leT by blast


lemma SKIP_FD_iff: ‹SKIP r ⊑⇩F⇩D P ⟷ P = SKIP r› for P :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof (rule iffI)
  show ‹P = SKIP r ⟹ SKIP r ⊑⇩F⇩D P› by simp
next
  show ‹P = SKIP r› if ‹SKIP r ⊑⇩F⇩D P›
  proof (rule FD_antisym[OF _ ‹SKIP r ⊑⇩F⇩D P›])
    show ‹P ⊑⇩F⇩D SKIP r›
    proof (rule failure_divergence_refineI)
      from ‹SKIP r ⊑⇩F⇩D P› show ‹s ∈ 𝒟 (SKIP r) ⟹ s ∈ 𝒟 P› for s
        by (simp add: refine_defs D_SKIP)
    next
      fix s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k› and X assume ‹(s, X) ∈ ℱ (SKIP r)›
      then consider ‹s = []› ‹✓(r) ∉ X› | ‹s = [✓(r)]› unfolding F_SKIP by blast
      thus ‹(s, X) ∈ ℱ P›
      proof cases
        from ‹SKIP r ⊑⇩F⇩D P› show ‹s = [] ⟹ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ P›
          by (simp add: refine_defs F_SKIP D_SKIP subset_iff)
            (metis T_F append_Nil is_processT1_TR is_processT5_S7 is_processT6_TR_notin not_Cons_self2)
      next
        from ‹SKIP r ⊑⇩F⇩D P› show ‹s = [✓(r)] ⟹ (s, X) ∈ ℱ P›
          by (simp add: refine_defs F_SKIP D_SKIP subset_iff)
            (metis (no_types) Int_insert_right_if0 is_processT1 list.simps(15) non_tickFree_tick
              tickFree_Nil tickFree_def tick_T_F trace_tick_continuation_or_all_tick_failuresE)
      qed
    qed
  qed
qed


lemma SKIP_F_iff: ‹SKIP r ⊑⇩F P ⟷ P = SKIP r›
proof (rule iffI)
  show ‹P = SKIP r ⟹ SKIP r ⊑⇩F P› by simp
next
  assume ‹SKIP r ⊑⇩F P›
  hence ‹SKIP r ⊑⇩D P›
    by (simp add: failure_refine_def divergence_refine_def subset_iff F_SKIP D_SKIP)
      (metis append_Nil equals0I insertI1 is_processT8 is_processT9 list.distinct(1))
  with ‹SKIP r ⊑⇩F P› have ‹SKIP r ⊑⇩F⇩D P› by (unfold failure_divergence_refine_def) simp
  thus ‹P = SKIP r› by (fact SKIP_FD_iff[THEN iffD1])
qed




(* TODO: prove a new version of this result, should be something like
  and move it
  ‹P ❙; Q = SKIP r ⟷ ∃S. (P = ⊓s ∈ S. SKIP s) ∧ (∀s ∈ S. Q s = SKIP r)› 

lemma Seq_is_SKIP_iff: ‹P ❙; Q = SKIP r ⟷ (∃s. P = SKIP s ∧ Q s = SKIP r)›
proof (intro iffI)
  show ‹∃s. P = SKIP s ∧ Q s = SKIP r ⟹ P ❙; Q = SKIP r›
    by (elim exE) (simp add: SKIP_Seq)
next
  assume ‹P ❙; Q = SKIP r›

  obtain s where ‹∃t ∈ 𝒯 P. tick s ∈ t›
  { fix t X assume ‹(t, X) ∈ ℱ P›
    hence ‹∃s. (t, X) ∈ ℱ (SKIP s)›
      sorry
  }
  then obtain s where ‹SKIP s ⊑⇩F P› unfolding failure_refine_def sledgehammer
  { fix t X assume ‹(t, X) ∈ ℱ (Q›
    hence ‹∃s. (t, X) ∈ ℱ (SKIP r)›
      sorry
  }
  hence ‹∃s. ›
  thus ‹∃s. P = SKIP s ∧ Q s = SKIP r›
    
    apply (simp add: Process_eq_spec F_Seq F_SKIP D_Seq D_SKIP, safe; simp)

  { fix s X
    assume ‹(s, X) ∈ ℱ P›
  hence ‹ℱ (P ❙; Q) = ℱ (SKIP r)› by simp
  thm this[simplified F_SKIP, simplified]
  thm this[simplified Process_eq_spec, simplified F_Seq D_Seq F_SKIP D_SKIP, simplified, simplified]
  apply (intro iffI, simp_all add: Seq_SKIP)
  apply (simp add: SKIP_F_iff[symmetric])
  unfolding failure_refine_def
proof (auto simp add: F_Seq F_SKIP D_Seq D_SKIP subset_iff intro: T_F, goal_cases)
  case (1 s X)
  thus ?case
    apply (cases ‹tickFree s›) 
     apply (erule_tac x = s in allE, 
            metis F_T append.right_neutral is_processT4_empty is_processT5_S4 process_charn)
    by (erule_tac x = ‹butlast s› in allE,
        metis F_T append.right_neutral append_butlast_last_id append_single_T_imp_tickFree
        last_snoc nonTickFree_n_frontTickFree non_tickFree_tick process_charn self_append_conv2)
next
  case (2 s X)
  thus ?case
    by (metis F_T append_Nil2 append_self_conv2 butlast_snoc front_tickFree_iff_tickFree_butlast
        insert_Diff insert_Diff_single nonTickFree_n_frontTickFree non_tickFree_tick process_charn)
qed (metis F_T append.left_neutral insertI1 insert_absorb2 is_processT5_S6 tickFree_Nil)+

 *)



(*<*)
end
  (*>*)