(*<*)
―‹ ********************************************************************
 * 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 ⊑_FD P' ==> Q ⊑_FD Q' ==> P ⊓ Q ⊑_FD P' ⊓ Q'›
  and mono_Ndet_DT : ‹P ⊑_DT P' ==> Q ⊑_DT Q' ==> P ⊓ Q ⊑_DT 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 ⊑_FD Q a) ==> (⊓a ∈ A. P a) ⊑_FD ⊓a ∈ A. Q a›
  and mono_GlobalNdet_DT : ‹(∧a. a ∈ A ==> P a ⊑_DT Q a) ==> (⊓a ∈ A. P a) ⊑_DT ⊓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) ⊑_FD (⊓a ∈ A. P a)›
  and GlobalNdet_DT_subset : ‹A ⊆ B ==> (⊓a ∈ B. P a) ⊑_DT (⊓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 ⊑_FD P' ==> Q ⊑_FD Q' ==> P ◻ Q ⊑_FD P' ◻ Q'›
proof (rule trans_FD)
  show ‹P ⊑_FD P' ==> P ◻ Q ⊑_FD P' ◻ Q›
    unfolding refine_defs F_Det D_Det using F_T T_F by blast
next
  show ‹Q ⊑_FD Q' ==> P' ◻ Q ⊑_FD 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 ⊑_DT P' ==> Q ⊑_DT Q' ==> P ◻ Q ⊑_DT 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 ⊑_FD P' ==> Q ⊑_FD Q' ==> P ⊳ Q ⊑_FD P' ⊳ Q'›
  and mono_Sliding_DT : ‹P ⊑_DT P' ==> Q ⊑_DT Q' ==> P ⊳ Q ⊑_DT 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 ⊑_FD P'; Q ⊑_FD Q'] ==> P [S] Q ⊑_FD P' [S] Q'›
  for P P' Q Q' :: ‹('a, 'r) process_ptick›
proof (rule trans_FD[of _ ‹P' [S] Q›])
  show ‹P [S] Q ⊑_FD P' [S] Q› if ‹P ⊑_FD P'› for P P' Q :: ‹('a, 'r) process_ptick›
  proof (rule failure_divergence_refine_optimizedI)
    from le_ref1 le_ref2T ‹P ⊑_FD P'›
    show ‹s ∈ D (P' [S] Q) ==> s ∈ D (P [S] Q)› for s
      unfolding D_Sync by blast
  next
    assume subset_div : ‹D (P' [S] Q) ⊆ D (P [S] Q)›
    fix s Z assume ‹(s, Z) ∈ F (P' [S] Q)›
    then consider ‹s ∈ D (P' [S] Q)›
      | (F) t u X Y where ‹(t, X) ∈ F P'› ‹(u, Y) ∈ F 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) ∈ F (P [S] Q)›
    proof cases
      from subset_div D_F show ‹s ∈ D (P' [S] Q) ==> (s, Z) ∈ F (P [S] Q)› by blast
    next
      case F
      with le_ref2[OF ‹P ⊑_FD P'›] show ‹(s, Z) ∈ F (P [S] Q)› unfolding F_Sync by blast
    qed
  qed
  thus ‹Q ⊑_FD Q' ==> P' [S] Q ⊑_FD P' [S] Q'› by (metis Sync_commute)
qed

lemma mono_Sync_DT : ‹P ⊑_DT P' ==> Q ⊑_DT Q' ==> P [S] Q ⊑_DT 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 ⊑_FD P' ==> Q ⊑_FD Q' ==> P ; Q ⊑_FD P' ; Q'›
  by (simp add: refine_defs Seq_projs subset_iff) (metis T_F_spec)

lemma mono_Seq_DT : ‹P ⊑_DT P' ==> Q ⊑_DT Q' ==> P ; Q ⊑_DT 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 ⊑_FD Q ==> Renaming P f g ⊑_FD Renaming Q f g›
  using mono_Renaming_D unfolding refine_defs F_Renaming D_Renaming by blast

lemma mono_Renaming_DT : ‹P ⊑_DT Q ==> Renaming P f g ⊑_DT 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 ∈ D (Q \ A)›
  then obtain t u
    where * : ‹front_tickFree u› ‹tickFree t›
      ‹s = trace_hide t (ev ` A) @ u›
      ‹t ∈ D 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 ∈ D 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 ∈ D Q› for i
        by (induct i) (simp_all add: ‹t ∈ D Q› is_processT7 tickFree_seqRun_iff "*"(2))
      thus ‹seqRun t (λi. ev a) i ∈ T P› for i
        by (meson D_T ‹P ⊑<sub>T</sub> 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 ∈ D (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) ∈ F (Q \ A)›
    then consider ‹s ∈ D (Q \ A)›
      | t where ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ F Q›
      unfolding F_Hiding_seqRun D_Hiding_seqRun by blast
    thus ‹(s, X) ∈ F (P \ A)›
    proof cases
      fix t assume ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ F Q›
      from ‹P ⊑_F Q› ‹(t, X ∪ ev ` A) ∈ F Q› have ‹(t, X ∪ ev ` A) ∈ F P›
        unfolding failure_refine_def by blast
      with ‹s = trace_hide t (ev ` A)› show ‹(s, X) ∈ F (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 ∈ D (Q \ A) ==> (s, X) ∈ F (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 ∈ T (Q \ A)›
    then consider ‹s ∈ D (Q \ A)›
      | t where ‹s = trace_hide t (ev ` A)› ‹(t, ev ` A) ∈ F Q›
      unfolding T_Hiding_seqRun D_Hiding_seqRun by blast
    thus ‹s ∈ T (P \ A)›
    proof cases
      fix t assume ‹s = trace_hide t (ev ` A)› ‹(t, ev ` A) ∈ F Q›
      from ‹(t, ev ` A) ∈ F Q› have ‹t ∈ T P›
        by (meson F_T ‹P ⊑<sub>T</sub> 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) ∈ F P›
      | f where ‹isInfHiddenRun f P A ∧ t ∈ range f› by blast
      thus ‹s ∈ T (P \ A)›
      proof cases
        show ‹trace_hide t' (ev ` A) = trace_hide t (ev ` A) ==>
 (t', ev ` A) ∈ F P ==> s ∈ T (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 ∈ T (P \ A)› for f
          by (simp add: T_Hiding)
            (metis T_nonTickFree_imp_decomp ‹s = trace_hide t (ev ` A)›
              ‹t ∈ 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 ∈ D (Q \ A) ==> s ∈ T (P \ A)›
        by (simp add: divergence_refine_def in_mono D_T)
    qed
  qed
qed

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

lemma mono_Hiding_DT : ‹P \ A ⊑_DT Q \ A› if ‹P ⊑_DT Q›
proof (cases ‹A = {}›)
  from ‹P ⊑_DT Q› show ‹A = {} ==> P \ A ⊑_DTQ \ A›
    by (auto simp add: refine_defs T_Hiding_seqRun D_Hiding_seqRun F_T T_F in_mono)
next
  show ‹A ≠ {} ==> P \ A ⊑_DT Q \ A›
    by (unfold trace_divergence_refine_def)
      (simp add: ‹P ⊑_DT 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 ⊑_FD Q a) ==> Mprefix A P ⊑_FD Mprefix A Q›
  and mono_Mprefix_DT : ‹(∧a. a ∈ A ==> P a ⊑_DT Q a) ==> Mprefix A P ⊑_DT 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 ⊑_FD Q ==> (a → P) ⊑_FD (a → Q)›
  and     mono_write0_DT : ‹P ⊑_DT Q ==> (a → P) ⊑_DT (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 ⊑_FD Q ==> (c!a → P) ⊑_FD (c!a → Q)›
  and     mono_write_DT : ‹P ⊑_DT Q ==> (c!a → P) ⊑_DT (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 ⊑_FD Q a) ==> (c?a∈A → P a) ⊑_FD (c?a∈A → Q a)›
  and     mono_read_DT : ‹(∧a. a ∈ A ==> P a ⊑_DT Q a) ==> (c?a∈A → P a) ⊑_DT (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 ⊑_FD Q a) ==> Mndetprefix A P ⊑_FD Mndetprefix A Q›
  and mono_Mndetprefix_DT : ‹(∧a. a ∈ A ==> P a ⊑_DT Q a) ==> Mndetprefix A P ⊑_DT 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 ⊑_FD Q a) ==> (c!!a∈A → P a) ⊑_FD (c!!a∈A → Q a)›
  and     mono_ndet_write_DT : ‹(∧a. a ∈ A ==> P a ⊑_DT Q a) ==> (c!!a∈A → P a) ⊑_DT (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 ⊑_FD Mprefix A P›
  and Mndetprefix_DT_Mprefix : ‹Mndetprefix A P ⊑_DT 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 ⊑_FD read c A P›
  and     ndet_write_DT_read : ‹ndet_write c A P ⊑_DT 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 ⊑_FD Mndetprefix A P›
  and Mndetprefix_DT_subset : ‹A ⊆ B ==> Mndetprefix B P ⊑_DT 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) ⊑_FD (c!!a∈A → P a)›
  and ndet_write_DT_subset : ‹(c!!b∈B → P b) ⊑_DT (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) ⊑_FD (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) ⊑_DT (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 ⊑_FD (a → P a)›
  and Mndetprefix_DT_write0 : ‹Mndetprefix A P ⊑_DT (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 ⊑_DT 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‹(⊑_FD)›
 where it holds for deterministic choice.›


lemma read_DT_subset : ‹(c?b∈B → P b) ⊑_DT (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) ⊑_DT (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 ⊑_FD P›
  and Ndet_DT_self_left   : ‹P ⊓ Q ⊑_DT 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 ⊑_FD Q›
  and Ndet_DT_self_right  : ‹P ⊓ Q ⊑_DT 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 ⊑_FD P ◻ Q›
  and Ndet_DT_Det : ‹P ⊓ Q ⊑_DT 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 ⊑_FD P ⊳ Q›
  and Ndet_DT_Sliding : ‹P ⊓ Q ⊑_DT 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 ⊑_FD P a›
  using GlobalNdet_FD_subset[of ‹{a}› A] by simp

lemma GlobalNdet_refine_DT : ‹a ∈ A ==> ⊓a ∈ A. P a ⊑_DT 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 ⊑_FD Q a) ==> P ⊑_FD ⊓a ∈ A. Q a›
  by (metis GlobalNdet_id mono_GlobalNdet_FD)

lemma mono_GlobalNdet_DT_const:
  ‹A ≠ {} ==> (∧a. a ∈ A ==> P ⊑_DT Q a) ==> P ⊑_DT ⊓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 ⊑_FD P ⟷ P = STOP›
  using STOP_F_iff leFD_imp_leF by blast

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


lemma SKIP_FD_iff: ‹SKIP r ⊑_FD P ⟷ P = SKIP r› for P :: ‹('a, 'r) process_ptick›
proof (rule iffI)
  show ‹P = SKIP r ==> SKIP r ⊑_FD P› by simp
next
  show ‹P = SKIP r› if ‹SKIP r ⊑_FD P›
  proof (rule FD_antisym[OF _ ‹SKIP r ⊑_FD P›])
    show ‹P ⊑_FD SKIP r›
    proof (rule failure_divergence_refineI)
      from ‹SKIP r ⊑_FD P› show ‹s ∈ D (SKIP r) ==> s ∈ D P› for s
        by (simp add: refine_defs D_SKIP)
    next
      fix s :: ‹('a, 'r) trace_ptick› and X assume ‹(s, X) ∈ F (SKIP r)›
      then consider ‹s = []› ‹🚫(r) ∉ X› | ‹s = [🚫(r)]› unfolding F_SKIP by blast
      thus ‹(s, X) ∈ F P›
      proof cases
        from ‹SKIP r ⊑_FD P› show ‹s = [] ==> 🚫(r) ∉ X ==> (s, X) ∈ F 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 ⊑_FD P› show ‹s = [🚫(r)] ==> (s, X) ∈ F 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 ⊑_FD 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
  \<open>P \<^bold>; Q = SKIP r \<longleftrightarrow> \<exists>S. (P = \<sqinter>s \<in> S. SKIP s) \<and> (\<forall>s \<in> S. Q s = SKIP r)\<close> 

lemma Seq_is_SKIP_iff: \<open>P \<^bold>; Q = SKIP r \<longleftrightarrow> (\<exists>s. P = SKIP s \<and> Q s = SKIP r)\<close>
proof (intro iffI)
  show \<open>\<exists>s. P = SKIP s \<and> Q s = SKIP r \<Longrightarrow> P \<^bold>; Q = SKIP r\<close>
    by (elim exE) (simp add: SKIP_Seq)
next
  assume \<open>P \<^bold>; Q = SKIP r\<close>

  obtain s where \<open>\<exists>t \<in> \<T> P. tick s \<in> t\<close>
  { fix t X assume \<open>(t, X) \<in> \<F> P\<close>
    hence \<open>\<exists>s. (t, X) \<in> \<F> (SKIP s)\<close>
      sorry
  }
  then obtain s where \<open>SKIP s \<sqsubseteq>\<^sub>F P\<close> unfolding failure_refine_def sledgehammer
  { fix t X assume \<open>(t, X) \<in> \<F> (Q\<close>
    hence \<open>\<exists>s. (t, X) \<in> \<F> (SKIP r)\<close>
      sorry
  }
  hence \<open>\<exists>s. \<close>
  thus \<open>\<exists>s. P = SKIP s \<and> Q s = SKIP r\<close>
    
    apply (simp add: Process_eq_spec F_Seq F_SKIP D_Seq D_SKIP, safe; simp)

  { fix s X
    assume \<open>(s, X) \<in> \<F> P\<close>
  hence \<open>\<F> (P \<^bold>; Q) = \<F> (SKIP r)\<close> 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 \<open>tickFree s\<close>) 
     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 = \<open>butlast s\<close> 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
  (*>*)