Theory ReadySet

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : Ready set of a process
 *
 * Copyright (c) 2023 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)

chapter ‹ The Ready Set Notion ›

theory  ReadySet
  imports Sliding Throw Interrupt
begin



text ‹This will be discussed more precisely later, but we want to define a new operator 
      which would in some way be the reciprocal of the prefix operator \<^term>‹e → P›.

      A first observation is that by prefixing \<^term>‹P› with \<^term>‹e›,
      we force its traces to begin with \<^term>‹ev e›.

      Therefore we must define a notion that captures this idea.›


text ‹We start by giving a notation to \<^const>‹tick› to be closer to Roscoe's 
      book \<^cite>‹"roscoe:csp:1998"› (and also closer to classic CSP literature).›

notation tick (‹✓›)


section ‹Definition›

text ‹The ready set notion captures the set of events that can be used to begin a given process.›

definition ready_set :: ‹'α process ⇒ 'α event set›
  where ‹ready_set P ≡ {a. [a] ∈ 𝒯 P}›

lemma ready_set_def_bis: ‹ready_set P = {e. ∃s. e # s ∈ 𝒯 P}›
  and Cons_in_T_imp_elem_ready_set: ‹e # s ∈ 𝒯 P ⟹ e ∈ ready_set P›
  unfolding ready_set_def using is_processT3_ST by force+


text ‹We say here that the \<^const>‹ready_set› of a process \<^term>‹P› is the set
      of events \<^term>‹e› such that there is a trace of \<^term>‹P› starting with \<^term>‹e›.

      One could also think about defining \<^term>‹ready_set P› as the set of events that
      \<^term>‹P› can not refuse at first: \<^term>‹{e. {e} ∉ ℛ P}›.
      These two definitions are not equivalent (and the second one is more restrictive
      than the first one). Moreover, the second does not behave well with the 
      non-deterministic choice \<^const>‹Ndet› (see the ⬚‹notepad› below).
      
      Therefore, we will keep the first one.

      We also have a strong argument of authority: this is the definition
      given by Roscoe (where it is called ‹initials›)
      \<^cite>‹‹p.40› in "Roscoe2010UnderstandingCS"›.›


notepad
begin
  fix e :: ‹'α event› ―‹just fixing \<^typ>‹'α› type›

  define bad_ready_set
    where ‹bad_ready_set (P :: 'α process) ≡ {e. {e} ∉ ℛ P}› for P

  have bad_ready_set_subset_ready_set:
    ‹bad_ready_set P ⊆ ready_set P› for P
    unfolding bad_ready_set_def ready_set_def Refusals_iff
    using F_T is_processT5_S6 by blast

  have bad_behaviour_with_Ndet: 
    ‹∃P Q. bad_ready_set (P ⊓ Q) ≠ bad_ready_set P ∪ bad_ready_set Q›
  proof (intro exI)
    show ‹bad_ready_set (SKIP ⊓ ⊥) ≠ bad_ready_set SKIP ∪ bad_ready_set ⊥›
    by (simp add: Ndet_BOT)
       (simp add: bad_ready_set_def F_Ndet F_SKIP F_UU Refusals_iff)
  qed
end



section ‹Anti-Mono Rules›

lemma anti_mono_ready_set_T: ‹P ⊑⇩T Q ⟹ ready_set Q ⊆ ready_set P›
  by (simp add: Collect_mono_iff trace_refine_def ready_set_def subsetD)

lemma anti_mono_ready_set_F: ‹P ⊑⇩F Q ⟹ ready_set Q ⊆ ready_set P›
  unfolding failure_refine_def
  by (drule F_subset_imp_T_subset) (fact anti_mono_ready_set_T[unfolded trace_refine_def])

text ‹Of course, this anti-monotony does not hold for \<^term>‹(⊑⇩D)›.›

lemma anti_mono_ready_set_FD: ‹P ⊑⇩F⇩D Q ⟹ ready_set Q ⊆ ready_set P›
  by (simp add: anti_mono_ready_set_F leFD_imp_leF)

lemma anti_mono_ready_set: ‹P ⊑ Q ⟹ ready_set Q ⊆ ready_set P›
  by (simp add: anti_mono_ready_set_T le_approx_lemma_T trace_refine_def)

lemma anti_mono_ready_set_DT: ‹P ⊑⇩D⇩T Q ⟹ ready_set Q ⊆ ready_set P›
  by (simp add: anti_mono_ready_set_T leDT_imp_leT)


section ‹Behaviour of \<^const>‹ready_set› with \<^const>‹STOP›, \<^const>‹SKIP› and \<^term>‹⊥››

lemma ready_set_STOP: ‹ready_set STOP = {}›
  by (simp add: ready_set_def T_STOP)

text ‹We already had @{thm STOP_iff_T}. As an immediate consequence we obtain a 
      characterization of being \<^const>‹STOP› involving \<^const>‹ready_set›.›

lemma ready_set_empty_iff_STOP: ‹ready_set P = {} ⟷ P = STOP›
proof (intro iffI)
  { assume ‹𝒯 P ≠ {[]}›
    then obtain a s where ‹a # s ∈ 𝒯 P› 
      by (metis Nil_elem_T is_singleton_the_elem is_singletonI'
                list.exhaust_sel singletonI empty_iff)
  hence ‹∃a. [a] ∈ 𝒯 P› by (metis append_Cons append_Nil is_processT3_ST)}
  thus ‹ready_set P = {} ⟹ P = STOP› 
    by (simp add: STOP_iff_T ready_set_def) presburger
qed (simp add: ready_set_STOP)


lemma ready_set_SKIP: ‹ready_set SKIP = {✓}›
  by (simp add: ready_set_def T_SKIP)

lemma ready_set_BOT: ‹ready_set ⊥ = UNIV›
  by (simp add: ready_set_def T_UU)

text ‹These two, on the other hand, are not characterizations.›

lemma ‹∃P. ready_set P = {✓} ∧ P ≠ SKIP›
proof (intro exI)
  show ‹ready_set (STOP ⊓ SKIP) = {✓} ∧ STOP ⊓ SKIP ≠ SKIP›
    by (simp add: ready_set_def T_Ndet T_STOP T_SKIP)
       (metis SKIP_F_iff SKIP_Neq_STOP idem_F mono_Ndet_F_left)
qed

lemma ‹∃P. ready_set P = UNIV ∧ P ≠ ⊥›
proof (intro exI)
  show ‹ready_set ((□a ∈ UNIV → ⊥) ⊓ SKIP) = UNIV ∧ (□a ∈ UNIV → ⊥) ⊓ SKIP ≠ ⊥›
  by (auto simp add: ready_set_def T_Ndet T_Mprefix Nil_elem_T T_SKIP
                     Ndet_is_BOT_iff SKIP_neq_BOT Mprefix_neq_BOT
              intro: event.exhaust)
qed



section ‹Behaviour of \<^const>‹ready_set› with Operators of \<^session>‹HOL-CSP››

lemma ready_set_Mprefix:     ‹ready_set (□a ∈ A → P a) = ev ` A›
  and ready_set_Mndetprefix: ‹ready_set (⊓a ∈ A → P a) = ev ` A›
  and ready_set_prefix:      ‹ready_set (a → Q)        = {ev a}›
  by (auto simp: ready_set_def T_Mndetprefix write0_def T_Mprefix Nil_elem_T)


text ‹As discussed earlier, \<^const>‹ready_set› behaves well with \<^term>‹(□)› and \<^term>‹(⊓)›.›

lemma ready_set_Det:  ‹ready_set (P □ Q) = ready_set P ∪ ready_set Q›
  and ready_set_Ndet: ‹ready_set (P ⊓ Q) = ready_set P ∪ ready_set Q›
  unfolding ready_set_def by (auto simp add: T_Det T_Ndet)


lemma ready_set_Seq: 
  ‹ready_set (P ❙; Q) = (if P = ⊥ then UNIV else ready_set P - {✓} ∪ 
                        (if ✓ ∈ ready_set P then ready_set Q else {}))›
proof -
  have ‹ready_set (P ❙; Q) = ready_set P› if ‹✓ ∉ ready_set P›
  proof (intro subset_antisym subsetI)
    fix e
    assume ‹e ∈ ready_set (P ❙; Q)›
    then obtain s where ‹e # s ∈ 𝒯 (P ❙; Q)› by (simp add: ready_set_def)
    then consider ‹e # s ∈ 𝒯 P›
      | ‹∃t1 t2. e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ t2 ∈ 𝒯 Q›
      by (simp add: T_Seq) (metis F_T NF_ND)
    thus ‹e ∈ ready_set P›
    proof cases
      show ‹e # s ∈ 𝒯 P ⟹ e ∈ ready_set P›
        by (simp add: Cons_in_T_imp_elem_ready_set)
    next
      assume ‹∃t1 t2. e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ t2 ∈ 𝒯 Q›
      then obtain t1 t2 where * : ‹e # s = t1 @ t2› ‹t1 @ [✓] ∈ 𝒯 P› by blast
      with that have ‹t1 ≠ [] ∧ hd t1 = e›
        by (metis Cons_in_T_imp_elem_ready_set append_Nil hd_append2 list.sel(1))
      thus ‹e ∈ ready_set P›
        by (metis Cons_in_T_imp_elem_ready_set "*"(2) is_processT3_ST list.exhaust_sel)
    qed
  next
    show ‹e ∈ ready_set P ⟹ e ∈ ready_set (P ❙; Q)› for e
      by (simp add: ready_set_def T_Seq)
         (metis Cons_in_T_imp_elem_ready_set Nil_elem_T that
                append.right_neutral is_processT5_S7 singletonD)
  qed
  also have ‹ready_set (P ❙; Q) = ready_set P - {✓} ∪ ready_set Q›
    if ‹P ≠ ⊥› and ‹✓ ∈ ready_set P›
  proof (intro subset_antisym subsetI)
    fix e
    assume ‹e ∈ ready_set (P ❙; Q)›
    then obtain s where ‹e # s ∈ 𝒯 (P ❙; Q)› by (simp add: ready_set_def)
    with ‹P ≠ ⊥› consider ‹e # s ∈ 𝒯 P› ‹e ≠ ✓›
      | ‹∃t1 t2. e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ t2 ∈ 𝒯 Q›
      by (simp add: T_Seq BOT_iff_D)
         (metis F_T append_T_imp_tickFree append_butlast_last_id butlast.simps(2) 
                last_ConsL list.distinct(1) process_charn tickFree_Cons)
    thus ‹e ∈ ready_set P - {✓} ∪ ready_set Q›
    proof cases
      show ‹e # s ∈ 𝒯 P ⟹ e ≠ ✓ ⟹ e ∈ ready_set P - {✓} ∪ ready_set Q›
        by (simp add: Cons_in_T_imp_elem_ready_set)
    next
      assume ‹∃t1 t2. e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ t2 ∈ 𝒯 Q›
      then obtain t1 t2 where * : ‹e # s = t1 @ t2› ‹t1 @ [✓] ∈ 𝒯 P› ‹t2 ∈ 𝒯 Q› by blast
      show ‹e ∈ ready_set P - {✓} ∪ ready_set Q›
      proof (cases t1)
        from "*"(1, 3) show ‹t1 = [] ⟹ e ∈ ready_set P - {✓} ∪ ready_set Q›
          using Cons_in_T_imp_elem_ready_set by auto
      next
        fix e' t1'
        assume ‹t1 = e' # t1'›
        with "*"(1, 2) have ‹t1 = e # t1' ∧ e ≠ ✓›
          by (metis append_T_imp_tickFree hd_append list.sel(1) neq_Nil_conv tickFree_Cons)
        with "*"(2) show ‹e ∈ ready_set P - {✓} ∪ ready_set Q›
          using Cons_in_T_imp_elem_ready_set by auto
      qed
    qed
  next
    fix e
    assume ‹e ∈ ready_set P - {✓} ∪ ready_set Q›
    then obtain s where ‹e ≠ ✓ ∧ e # s ∈ 𝒯 P ∨ e # s ∈ 𝒯 Q›
      unfolding ready_set_def by blast
    thus ‹e ∈ ready_set (P ❙; Q)›
    proof (elim disjE conjE)
      show ‹e ≠ ✓ ⟹ e # s ∈ 𝒯 P ⟹ e ∈ ready_set (P ❙; Q)›
        by (simp add: ready_set_def T_Seq)
           (metis Nil_elem_T append_Cons append_Nil
                  is_processT3_ST is_processT5_S7 singletonD)
    next
      have ‹[✓] ∈ 𝒯 P› using ready_set_def that(2) by auto
      thus ‹e # s ∈ 𝒯 Q ⟹ e ∈ ready_set (P ❙; Q)›
        by (simp add: ready_set_def T_Seq)
           (metis append_Cons append_Nil is_processT3_ST)
    qed
  qed
  ultimately show ?thesis by (simp add: BOT_Seq ready_set_BOT)
qed
  
  

lemma ready_set_Sync:
  ‹ready_set (P ⟦S⟧ Q) =
   (  if P = ⊥ ∨ Q = ⊥ then UNIV
    else (ready_set P - insert ✓ (ev ` S)) ∪ 
         (ready_set Q - insert ✓ (ev ` S)) ∪
          ready_set P ∩ ready_set Q ∩ insert ✓ (ev ` S))›
  (is ‹ready_set (P ⟦S⟧ Q) = (if P = ⊥ ∨ Q = ⊥ then UNIV else ?rhs)›)
proof -
  have ‹ready_set (P ⟦S⟧ Q) = ?rhs› if non_BOT : ‹P ≠ ⊥› ‹Q ≠ ⊥›
  proof (intro subset_antisym subsetI)
    show ‹e ∈ ?rhs ⟹ e ∈ ready_set (P ⟦S⟧ Q)› for e
      by (use Nil_elem_T in ‹fastforce simp add: ready_set_def T_Sync›)
  next
    fix e
    assume ‹e ∈ ready_set (P ⟦S⟧ Q)›
    then consider ‹∃t u. t ∈ 𝒯 P ∧ u ∈ 𝒯 Q ∧ [e] setinterleaves ((t, u), insert ✓ (ev ` S))›
      | ‹∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧ [e] = r @ v ∧
                   r setinterleaves ((t, u), insert ✓ (ev ` S)) ∧
                   (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)›
      by (simp add: ready_set_def T_Sync) blast
    thus ‹e ∈ ?rhs›
    proof cases
      assume ‹∃t u. t ∈ 𝒯 P ∧ u ∈ 𝒯 Q ∧ [e] setinterleaves ((t, u), insert ✓ (ev ` S))›
      then obtain t u where assms : ‹t ∈ 𝒯 P› ‹u ∈ 𝒯 Q› 
                                    ‹[e] setinterleaves ((t, u), insert ✓ (ev ` S))› by blast
      thus ‹e ∈ ?rhs›
        apply (cases t; cases u; simp add: ready_set_def split: if_split_asm)
        using empty_setinterleaving Sync.sym by blast+
    next
      assume ‹∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧ [e] = r @ v ∧
                        r setinterleaves ((t, u), insert ✓ (ev ` S)) ∧
                        (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)› 
      then obtain t u r v
        where * : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹[e] = r @ v›
                  ‹r setinterleaves ((t, u), insert ✓ (ev ` S))›
                  ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P› by blast
      have ‹r ≠ []› using "*"(4, 5) BOT_iff_D empty_setinterleaving that by blast
      hence ‹r = [e] ∧ v = []›
        by (metis (no_types, lifting) "*"(3) Nil_is_append_conv append_eq_Cons_conv)
      also obtain e' t' where ‹t = e' # t'›
        using "*"(5) BOT_iff_D non_BOT by (cases t; blast)
      ultimately show ‹e ∈ ?rhs› 
        using "*"(4, 5) apply (simp add: ready_set_def subset_iff T_Sync)
        apply (cases u; simp split: if_split_asm)
        by (metis (no_types, opaque_lifting) [[metis_verbose = false]]
                   D_T Sync.sym empty_setinterleaving)+
    qed
  qed
  thus ‹ready_set (P ⟦S⟧ Q) = (if P = ⊥ ∨ Q = ⊥ then UNIV else ?rhs)›
    by (simp add: Sync_BOT Sync_commute[of ⊥, simplified Sync_BOT] ready_set_BOT)
qed


lemma ready_set_Renaming:
  ‹ready_set (Renaming P f) = (if P = ⊥ then UNIV else EvExt f ` (ready_set P))›
proof -
  { fix y t1 t2
    assume assms: ‹[] ∉ 𝒟 P› ‹[y] = map (EvExt f) t1 @ t2› ‹t1 ∈ 𝒟 P›
    from assms have ‹t2 = []›
      by (metis Nil_is_append_conv list.map_disc_iff list.sel(3) tl_append2)
    with assms(2) D_T[OF assms(3)] have ‹∃x. [x] ∈ 𝒯 P ∧ y = EvExt f x› by auto
  }
  thus ?thesis by (auto simp add: ready_set_def T_Renaming image_iff BOT_iff_D)
qed




text ‹Because for the expression of its traces (and more specifically of its divergences),
      dealing with \<^const>‹Hiding› is much more difficult.›

text ‹We start with two characterizations:
      ▪ one to understand \<^prop>‹P \ S = ⊥›
      ▪ the other to understand \<^prop>‹[e] ∈ 𝒟 (P \ S)›.›

lemma Hiding_is_BOT_iff : 
  ‹P \ S = ⊥ ⟷ (∃t. set t ⊆ ev ` S ∧ 
                      (t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P S ∧ t ∈ range f)))›
  (is ‹P \ S = ⊥ ⟷ ?rhs›)
proof (subst BOT_iff_D, intro iffI)
  show ‹[] ∈ 𝒟 (P \ S) ⟹ ?rhs›
    by (simp add: D_Hiding)
       (metis (no_types, lifting) filter_empty_conv subsetI)
next
  assume ‹?rhs›
  then obtain t where * : ‹set t ⊆ ev ` S›
                          ‹t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P S ∧ t ∈ range f)› by blast
  hence ‹tickFree t ∧ [] = trace_hide t (ev ` S)›
    unfolding tickFree_def by (auto simp add: D_Hiding subset_iff)
  with "*"(2) show ‹[] ∈ 𝒟 (P \ S)› by (simp add: D_Hiding) metis
qed

lemma event_in_D_Hiding_iff :
  ‹[e] ∈ 𝒟 (P \ S) ⟷
   P \ S = ⊥ ∨ (∃x t. e = ev x ∧ x ∉ S ∧ [ev x] = trace_hide t (ev ` S) ∧
                      (t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P S ∧ t ∈ range f)))›
  (is ‹[e] ∈ 𝒟 (P \ S) ⟷ P \ S = ⊥ ∨ ?ugly_assertion›)
proof (intro iffI)
  assume assm : ‹[e] ∈ 𝒟 (P \ S)›
  show ‹P \ S = ⊥ ∨ ?ugly_assertion›
  proof (cases e)
    assume ‹e = ✓›
    with assm have ‹P \ S = ⊥›
      using BOT_iff_D front_tickFree_Nil is_processT9_tick by blast
    thus ‹P \ S = ⊥ ∨ ?ugly_assertion› by blast
  next
    fix x
    assume ‹e = ev x›
    with assm obtain t u
      where * : ‹front_tickFree u› ‹tickFree t›
                ‹[ev x] = trace_hide t (ev ` S) @ u›
                ‹t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P S ∧ t ∈ range f)›
      by (simp add: D_Hiding) blast
    from "*"(3) consider ‹set t ⊆ ev ` S› | ‹x ∉ S› ‹ev x ∈ set t›
      by (metis (no_types, lifting) Cons_eq_append_conv empty_filter_conv
          filter_eq_Cons_iff filter_is_subset image_eqI list.set_intros(1) subset_code(1))
    thus ‹P \ S = ⊥ ∨ ?ugly_assertion›
    proof cases
      assume ‹set t ⊆ ev ` S›
      hence ‹P \ S = ⊥› by (meson "*"(4) Hiding_is_BOT_iff)
      thus ‹P \ S = ⊥ ∨ ?ugly_assertion› by blast
    next
      assume ‹x ∉ S› ‹ev x ∈ set t›
      with "*"(3) have ‹[ev x] = trace_hide t (ev ` S)›
        by (induct t) (auto split: if_split_asm)
      with "*"(4) ‹e = ev x› ‹x ∉ S› have ‹?ugly_assertion› by blast
      thus ‹P \ S = ⊥ ∨ ?ugly_assertion› by blast
    qed
  qed
next
  show ‹P \ S = ⊥ ∨ ?ugly_assertion ⟹ [e] ∈ 𝒟 (P \ S)›
  proof (elim disjE)
    show ‹P \ S = ⊥ ⟹ [e] ∈ 𝒟 (P \ S)› by (simp add: D_UU)
  next
    show ‹?ugly_assertion ⟹ [e] ∈ 𝒟 (P \ S)›
      by (elim exE, simp add: D_Hiding)
         (metis Hiding_tickFree append_Nil2 event.simps(3)
                front_tickFree_Nil tickFree_Cons tickFree_Nil)
  qed
qed


text ‹Now we can express \<^term>‹ready_set (P \ S)›.
      This result contains the term \<^term>‹P \ S = ⊥› that can be unfolded with
      @{thm [source] Hiding_is_BOT_iff} and the term \<^term>‹[ev x] ∈ 𝒟 (P \ S)›
      that can be unfolded with @{thm [source] event_in_D_Hiding_iff}.›

lemma ready_set_Hiding:
  ‹ready_set (P \ S) = 
   (if P \ S = ⊥ then UNIV else
    {e. case e of ✓ ⇒ ∃t. set t ⊆ ev ` S ∧ t @ [✓] ∈ 𝒯 P
        | ev x ⇒ x ∉ S ∧ ([ev x] ∈ 𝒟 (P \ S) ∨ 
                           (∃t. [ev x] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ ℱ P))})›
  (is ‹ready_set (P \ S) = (if P \ S = ⊥ then UNIV else ?set)›)
proof (split if_split, intro conjI impI)
  show ‹P \ S = ⊥ ⟹ ready_set (P \ S) = UNIV› by (simp add: ready_set_BOT)
next
  assume non_BOT : ‹P \ S ≠ ⊥›
  show ‹ready_set (P \ S) = ?set›
  proof (intro subset_antisym subsetI)
    fix e
    assume ready : ‹e ∈ ready_set (P \ S)›
    ― ‹This implies \<^prop>‹e ∉ ev ` S› with our other assumptions.›
    { fix x
      assume assms : ‹x ∈ S› ‹ev x ∈ ready_set (P \ S)›
      then consider ‹∃t. [ev x] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ ℱ P›
        | ‹∃t u. front_tickFree u ∧ tickFree t ∧ [ev x] = trace_hide t (ev ` S) @ u ∧ 
                 (t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P S ∧ t ∈ range f))›
        by (simp add: ready_set_def T_Hiding) blast
      hence ‹P \ S = ⊥›
      proof cases
        assume ‹∃t. [ev x] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ ℱ P›
        hence False by (metis Cons_eq_filterD image_eqI assms(1))
        thus ‹P \ S = ⊥› by blast
      next
        assume ‹∃t u. front_tickFree u ∧ tickFree t ∧ [ev x] = trace_hide t (ev ` S) @ u ∧
                      (t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P S ∧ t ∈ range f))›
        then obtain t u 
          where * : ‹front_tickFree u› ‹tickFree t› ‹[ev x] = trace_hide t (ev ` S) @ u›
                    ‹t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P S ∧ t ∈ range f)› by blast
        from *(3) have ** : ‹set t ⊆ ev ` S›
          by (induct t) (simp_all add: assms(1) split: if_split_asm)
        from *(4) "**" Hiding_is_BOT_iff show ‹P \ S = ⊥› by blast
      qed
    }
    with ready have * : ‹e ∉ ev ` S› using non_BOT by blast

    from ready consider ‹[e] ∈ 𝒟 (P \ S)›
      | ‹∃t. [e] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ ℱ P›
      unfolding ready_set_def by (simp add: T_Hiding D_Hiding) blast
    thus ‹e ∈ ?set›
    proof cases
      assume assm : ‹[e] ∈ 𝒟 (P \ S)›
      then obtain x where ‹e = ev x›
        ― ‹because \<^prop>‹[tick] ∈ 𝒟 (P \ S) ⟹ P \ S = ⊥››
        by (metis BOT_iff_D append_Nil event.exhaust non_BOT process_charn)
      with assm "*" show ‹e ∈ ?set› by (simp add: image_iff)
    next
      assume ‹∃t. [e] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ ℱ P›
      then obtain t where ** : ‹[e] = trace_hide t (ev ` S)›
                               ‹(t, ev ` S) ∈ ℱ P› by blast
      thus ‹e ∈ ?set›
      proof (cases e)
        have ‹e = ✓ ⟹ set (butlast t) ⊆ ev ` S ∧ butlast t @ [✓] ∈ 𝒯 P›
          using "**" apply (cases t rule: rev_cases; simp add: split: if_split_asm)
          by (metis F_T filter_empty_conv subset_code(1))
             (metis Hiding_tickFree front_tickFree_implies_tickFree process_charn tickFree_Cons)
        thus ‹e = ✓ ⟹ e ∈ ?set› by auto
      next
        fix x
        assume ‹e = ev x›
        with "*" have ‹x ∉ S› by blast
        with ‹e = ev x› "**"(1) "**"(2) show ‹e ∈ ?set› by auto
      qed
    qed
  next
    fix e
    assume ‹e ∈ ?set›
    then consider ‹e = ✓› ‹∃t. set t ⊆ ev ` S ∧ t @ [✓] ∈ 𝒯 P›
      | ‹∃x. e = ev x ∧ x ∉ S ∧
             ([ev x] ∈ 𝒟 (P \ S) ∨
              (∃t. [ev x] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ ℱ P))› by (cases e; simp)
    thus ‹e ∈ ready_set (P \ S)›
    proof cases
      assume assms : ‹e = ✓› ‹∃t. set t ⊆ ev ` S ∧ t @ [✓] ∈ 𝒯 P›
      from assms(2) obtain t
        where * : ‹set t ⊆ ev ` S› ‹t @ [✓] ∈ 𝒯 P› by blast
      have ** : ‹[e] = trace_hide (t @ [✓]) (ev ` S) ∧ (t @ [✓], ev ` S) ∈ ℱ P›
        using "*"(1) by (simp add: assms(1) image_iff tick_T_F[OF "*"(2)] subset_iff)
      show ‹e ∈ ready_set (P \ S)›
        unfolding ready_set_def by (simp add: T_Hiding) (use "**" in blast)
    next
      show ‹∃x. e = ev x ∧ x ∉ S ∧
             ([ev x] ∈ 𝒟 (P \ S) ∨
              (∃t. [ev x] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ ℱ P)) ⟹
            e ∈ ready_set (P \ S)›
        apply (elim exE conjE disjE)
        using Cons_in_T_imp_elem_ready_set D_T apply blast
        unfolding ready_set_def by (simp add: T_Hiding) blast
    qed
  qed
qed


text ‹In the end the result would look something like this:

      @{thm ready_set_Hiding[unfolded event_in_D_Hiding_iff Hiding_is_BOT_iff, no_vars]}›

text ‹Obviously, it is not very easy to use. We will therefore rely more on the corollaries below.›
 
corollary ready_tick_Hiding_iff :
  ‹✓ ∈ ready_set (P \ B) ⟷ P \ B = ⊥ ∨ (∃t. set t ⊆ ev ` B ∧ t @ [✓] ∈ 𝒯 P)›
  by (simp add: ready_set_Hiding)

corollary ready_tick_imp_ready_tick_Hiding:
  ‹✓ ∈ ready_set P ⟹ ✓ ∈ ready_set (P \ B)›
  by (subst ready_set_Hiding, simp add: ready_set_def)
     (metis append_Nil empty_iff empty_set subset_iff)


corollary ready_inside_Hiding_iff :
  ‹e ∈ S ⟹ ev e ∈ ready_set (P \ S) ⟷ P \ S = ⊥›
  by (simp add: ready_set_Hiding)


corollary ready_notin_Hiding_iff :
  ‹e ∉ S ⟹ ev e ∈ ready_set (P \ S) ⟷
   P \ S = ⊥ ∨
   (∃t. [ev e] = trace_hide t (ev ` S) ∧
        (t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P S ∧ t ∈ range f) ∨ (t, ev ` S) ∈ ℱ P))›
  by (auto simp add: ready_set_Hiding event_in_D_Hiding_iff split: if_split_asm)


corollary ready_notin_imp_ready_Hiding:
  ‹ev e ∈ ready_set (P \ S)› if ready : ‹ev e ∈ ready_set P› and notin : ‹e ∉ S›
proof -
  from inf_hidden[of S ‹[ev e]› P]
  consider ‹∃f. isInfHiddenRun f P S ∧ [ev e] ∈ range f›  
    | ‹∃t. [ev e] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ ℱ P›
    by (simp add: ready_set_Hiding image_iff[of ‹ev e›] notin)
       (metis mem_Collect_eq ready ready_set_def)
  thus ‹ev e ∈ ready_set (P \ S)›
  proof cases
    show ‹∃f. isInfHiddenRun f P S ∧ [ev e] ∈ range f ⟹ ev e ∈ ready_set (P \ S)›
      apply (rule Cons_in_T_imp_elem_ready_set[of ‹ev e› ‹[]›], rule D_T)
      apply (simp add: event_in_D_Hiding_iff image_iff[of ‹ev e›] notin)
      by (metis (no_types, lifting) event.inject filter.simps image_iff notin)
  next
    assume ‹∃t. [ev e] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ ℱ P›
    thus ‹ev e ∈ ready_set (P \ S)› by (simp add: ready_set_Hiding notin)
  qed
qed


(* old proofs below 

lemma tick_not_hidden_ready_set_Hiding:
  ‹✓ ∈ ready_set P ⟹ ✓ ∈ ready_set (P \ B)›
  by (simp add: ready_set_def T_Hiding)
     (metis (no_types, lifting) append_Nil event.simps(3) filter.simps image_iff tick_T_F)


lemma ready_notin_ready_Hiding:
  ‹ev e ∈ ready_set P ⟹ e ∉ B ⟹ ev e ∈ ready_set (P \ B)›
proof -
  have ‹∃ t u. front_tickFree u ∧ tickFree t ∧ [ev e] = trace_hide t (ev ` B) @ u ∧ 
               (t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P B ∧ t ∈ range f))›
    if a1 : ‹[ev e] ∈ 𝒯 P› and a2 : ‹e ∉ B› 
   and a3 : ‹∀t. [ev e] = trace_hide t (ev ` B) ⟶ (t, ev ` B) ∉ ℱ P›
  proof -
    have   * : ‹[ev e] = trace_hide [ev e] (ev ` B)› by (simp add: a2 image_iff)
    hence ** : ‹∀t. trace_hide t (ev ` B) = trace_hide [ev e] (ev ` B) ⟶ (t, ev ` B) ∉ ℱ P›
      using a3 by presburger
    show ‹∃ t u. front_tickFree u ∧ tickFree t ∧ [ev e] = trace_hide t (ev ` B) @ u ∧ 
                 (t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P B ∧ t ∈ range f))›
      apply (rule_tac x = ‹[ev e]› in exI, rule_tac x = ‹[]› in exI, intro conjI)
         apply simp
        apply simp
       apply (simp only: append_Nil2, rule "*")
      by (rule disjI2, rule inf_hidden[OF ** a1])
  qed
  thus ‹ev e ∈ ready_set P ⟹ e ∉ B ⟹ ev e ∈ ready_set (P \ B)›
    by (auto simp add: ready_set_def T_Hiding)
qed


lemma ready_Hiding_inside_iff : 
  ‹ev e ∈ ready_set (P \ B) ⟷  
   (∃t. set t ⊆ ev ` B ∧
   (t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P B ∧ t ∈ range f)))› (is ‹?lhs ⟷ ?rhs›)
  if inside : ‹e ∈ B›
proof (intro iffI)
  assume ?lhs
  then consider ‹∃t. [ev e] = trace_hide t (ev ` B) ∧ (t, ev `B) ∈ ℱ P›
    | ‹∃t u. front_tickFree u ∧ tickFree t ∧ [ev e] = trace_hide t (ev ` B) @ u ∧ 
             (t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P B ∧ t ∈ range f))›
    by (simp add: ready_set_def T_Hiding) blast
  thus ?rhs
  proof cases
    assume ‹∃t. [ev e] = trace_hide t (ev ` B) ∧ (t, ev ` B) ∈ ℱ P›
    hence False by (metis Cons_eq_filterD image_eqI inside)
    thus ?rhs by blast
  next
    assume ‹∃t u. front_tickFree u ∧ tickFree t ∧ [ev e] = trace_hide t (ev ` B) @ u ∧ 
                  (t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P B ∧ t ∈ range f))›
    then obtain t u 
      where * : ‹front_tickFree u› ‹tickFree t› ‹[ev e] = trace_hide t (ev ` B) @ u›
                ‹t ∈ 𝒟 P ∨ (∃ f. isInfHiddenRun f P B ∧ t ∈ range f)› by blast
    from *(3) have ** : ‹set t ⊆ insert ✓ (ev ` B)›
      by (induct t) (simp_all add: inside split: if_split_asm)
    from *(4) show ?rhs by (rule_tac x = t in exI)
                           (meson "*"(2) "**" subset_insert tickFree_def)
  qed
next
  assume ?rhs
  then obtain t
    where * : ‹set t ⊆ ev ` B›
              ‹t ∈ 𝒟 P ∨ (∃f. isInfHiddenRun f P B ∧ t ∈ range f)› by blast
  show ?lhs
    apply (simp add: ready_set_def T_Hiding)
    apply (rule disjI2)
    apply (rule_tac x = t in exI, rule_tac x = ‹[ev e]› in exI, simp, intro conjI)
      apply (meson "*"(1) event.simps(3) image_iff subsetD tickFree_def)
     apply (meson "*"(1) filter_False subset_eq)
    using "*"(2) by blast
qed *)
  
  


section ‹Behaviour of \<^const>‹ready_set› with Operators of \<^session>‹HOL-CSPM››
  
lemma ready_set_MultiDet:
  ‹finite A ⟹ ready_set (MultiDet A P) = (⋃a ∈ A. ready_set (P a))›
  by (induct A rule: finite_induct)
     (simp_all add: ready_set_STOP ready_set_Det)


lemma ready_set_MultiNdet:
  ‹finite A ⟹ ready_set (MultiNdet A P) = (⋃a ∈ A. ready_set (P a))›
  apply (cases ‹A = {}›, simp add: ready_set_STOP)
  by (rotate_tac, induct A rule: finite_set_induct_nonempty)
     (simp_all add: ready_set_Ndet)


lemma ready_set_GlobalNdet:
  ‹ready_set (GlobalNdet A P) = (⋃a ∈ A. ready_set (P a))›
  by (auto simp add: ready_set_def T_GlobalNdet)


lemma ready_set_MultiSeq:
  ‹ready_set (MultiSeq L P) =
   (  if L = [] then {✓}
    else   if P (hd L) = ⊥ then UNIV
         else   if ✓ ∈ ready_set (P (hd L)) 
              then ready_set (P (hd L)) - {✓} ∪ ready_set (MultiSeq (tl L) P)
              else ready_set (P (hd L)))›
  by (induct L) (simp_all add: ready_set_SKIP ready_set_Seq)


lemma ready_set_MultiSync:
  ‹ready_set (❙⟦S❙⟧ m ∈# M. P m) =
   (  if M = {#} then {}
    else if ∃m ∈# M. P m = ⊥ then UNIV
    else if ∃m. M = {#m#} then ready_set (P (THE m. M = {#m#}))
    else {e. ∃m ∈# M. e ∈ ready_set (P m) - insert ✓ (ev ` S)} ∪
         {e ∈ insert ✓ (ev ` S). ∀m ∈# M. e ∈ ready_set (P m)})›
proof -
  have * : ‹ready_set (❙⟦S❙⟧ m ∈# M + {#a, a'#}. P m) = 
            {e. ∃m ∈# M + {#a, a'#}. e ∈ ready_set (P m) - insert ✓ (ev ` S)} ∪
            {e ∈ insert ✓ (ev ` S). ∀m ∈# M + {#a, a'#}. e ∈ ready_set (P m)}›
    if non_BOT : ‹∀m ∈# M + {#a, a'#}. P m ≠ ⊥› for a a' M
  proof (induct M rule: msubset_induct'[OF subset_mset.refl])
    case 1
    then show ?case by (auto simp add: non_BOT ready_set_Sync)
  next
    case (2 a'' M')
    have * : ‹MultiSync S (add_mset a'' M' + {#a, a'#}) P = 
              P a'' ⟦S⟧ (MultiSync S (M' + {#a, a'#}) P)› 
      by (simp add: add_mset_commute)
    have ** : ‹¬ (P a'' = ⊥ ∨ MultiSync S (M' + {#a, a'#}) P = ⊥)›
      using "2.hyps"(1, 2) in_diffD non_BOT 
      by (auto simp add: MultiSync_is_BOT_iff Sync_is_BOT_iff, fastforce, meson mset_subset_eqD)
    show ?case
      by (auto simp only: * ready_set_Sync ** "2.hyps"(3), auto)
  qed

  show ?thesis
  proof (cases ‹∃m ∈# M. P m = ⊥›)
    show ‹∃m ∈# M. P m = ⊥ ⟹ ?thesis›
      by (simp add: ready_set_STOP) (metis MultiSync_BOT_absorb ready_set_BOT)
  next
    show ‹¬ (∃m∈#M. P m = ⊥) ⟹ ?thesis›
    proof (cases ‹∃a a' M'. M = M' + {#a, a'#}›)
      assume assms : ‹¬ (∃m∈#M. P m = ⊥)› ‹∃a a' M'. M = M' + {#a, a'#}›
      from assms(2) obtain a a' M' where ‹M = M' + {#a, a'#}› by blast
      with * assms(1) show ?thesis by simp
    next
      assume ‹∄a a' M'. M = M' + {#a, a'#}›
      hence ‹M = {#} ∨ (∃m. M = {#m#})›
        by (metis add.right_neutral multiset_cases union_mset_add_mset_right)
      thus ?thesis by (auto simp add: ready_set_STOP ready_set_BOT)
    qed
  qed
qed


 
section ‹Behaviour of \<^const>‹ready_set› with Operators of \<^session>‹HOL-CSP_OpSem››

lemma ready_set_Sliding: 
  ‹ready_set (P ⊳ Q) = ready_set P ∪ ready_set Q›
  unfolding ready_set_def by (auto simp add: T_Sliding)


lemma ready_set_Throw: ‹ready_set (P Θ a ∈ A. Q a) = ready_set P›
  apply (intro subset_antisym subsetI;
      simp add: ready_set_def T_Throw image_iff)
   apply (elim disjE)
     apply (solves ‹simp›)
    apply (metis D_T process_charn)
   apply (metis Nil_is_append_conv list.sel(3) neq_Nil_conv self_append_conv2 tl_append2)
  by (metis Nil_elem_T append_Nil empty_set inf_bot_left)
 

corollary Throw_is_STOP_iff: ‹P Θ a ∈ A. Q a = STOP ⟷ P = STOP›
  by (simp add: ready_set_empty_iff_STOP[symmetric] ready_set_Throw)


lemma ready_set_Interrupt: ‹ready_set (P △ Q) = ready_set P ∪ ready_set Q›
  apply (intro subset_antisym subsetI;
         simp add: ready_set_def T_Interrupt)
  by (metis Nil_is_append_conv append.left_neutral 
            append.right_neutral butlast.simps(2) butlast_append)
     (use Nil_elem_T tickFree_Nil in blast)

corollary Interrupt_is_STOP_iff: ‹P △ Q = STOP ⟷ P = STOP ∧ Q = STOP›
  by (simp add: ready_set_empty_iff_STOP[symmetric] ready_set_Interrupt)



section ‹Behaviour of \<^const>‹ready_set› with Reference Processes›

lemma ready_set_DF: ‹ready_set (DF A) = ev ` A›
  by (subst DF_unfold) (simp add: ready_set_Mndetprefix)

lemma ready_set_DF⇩S⇩K⇩I⇩P: ‹ready_set (DF⇩S⇩K⇩I⇩P A) = insert ✓ (ev ` A)›
  by (subst DF⇩S⇩K⇩I⇩P_unfold)
     (simp add: ready_set_Mndetprefix ready_set_Ndet ready_set_SKIP)

lemma ready_set_RUN: ‹ready_set (RUN A) = ev ` A›
  by (subst RUN_unfold) (simp add: ready_set_Mprefix)

lemma ready_set_CHAOS: ‹ready_set (CHAOS A) = ev ` A›
  by (subst CHAOS_unfold)
     (simp add: ready_set_Mprefix ready_set_Ndet ready_set_STOP)

lemma ready_set_CHAOS⇩S⇩K⇩I⇩P: ‹ready_set (CHAOS⇩S⇩K⇩I⇩P A) = insert ✓ (ev ` A)›
  by (subst CHAOS⇩S⇩K⇩I⇩P_unfold)
     (simp add: ready_set_Mprefix ready_set_Ndet
                ready_set_STOP ready_set_SKIP)



end