Theory Events_Ticks_CSP_Laws

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

chapter ‹Events and Ticks of a Process›

(*<*)
theory Events_Ticks_CSP_Laws
  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
  (*>*)

section ‹Definitions›

subsection ‹Events of a Process›

definition events_of :: ‹('a, 'r) processptick ⇒ 'a set› (‹α'(_')›)
  ―‹term‹α(P)› for ``alphabet of term‹P›''›
  where ‹α(P) ≡ ⋃t∈𝒯 P. {a. ev a ∈ set t}›

lemma events_of_memI : ‹t ∈ 𝒯 P ⟹ ev a ∈ set t ⟹ a ∈ α(P)›
  unfolding events_of_def by blast

lemma events_of_memD : ‹a ∈ α(P) ⟹ ∃t ∈ 𝒯 P. ev a ∈ set t›
  unfolding events_of_def by blast

lemma events_of_memE :
  ‹a ∈ α(P) ⟹ (⋀t. t ∈ 𝒯 P ⟹ ev a ∈ set t ⟹ thesis) ⟹ thesis›
  by (meson events_of_memD)


definition strict_events_of :: ‹('a, 'r) processptick ⇒ 'a set› (‹α'(_')›)
  where ‹α(P) ≡ ⋃t∈𝒯 P - 𝒟 P. {a. ev a ∈ set t}›

lemma strict_events_of_memI :
  ‹t ∈ 𝒯 P ⟹ t ∉ 𝒟 P ⟹ ev a ∈ set t ⟹ a ∈ α(P)›
  unfolding strict_events_of_def by blast

lemma strict_events_of_memD : ‹a ∈ α(P) ⟹ ∃t ∈ 𝒯 P. t ∉ 𝒟 P ∧ ev a ∈ set t›
  unfolding strict_events_of_def by blast

lemma strict_events_of_memE :
  ‹a ∈ α(P) ⟹ (⋀t. t ∈ 𝒯 P ⟹ t ∉ 𝒟 P ⟹ ev a ∈ set t ⟹ thesis) ⟹ thesis›
  by (meson strict_events_of_memD)


lemma events_of_is_strict_events_of_or_UNIV :
  ‹α(P) = (if 𝒟 P = {} then α(P) else UNIV)›
proof (split if_split, intro conjI impI)
  show ‹𝒟 P = {} ⟹ α(P) = α(P)› by (simp add: events_of_def strict_events_of_def)
next
  assume ‹𝒟 P ≠ {}›
  with nonempty_divE obtain t where ‹tF t› ‹t ∈ 𝒟 P› by blast
  hence ‹t @ [ev a] ∈ 𝒟 P› for a by (simp add: is_processT7)
  thus ‹α(P) = UNIV› by (metis D_T UNIV_eq_I events_of_memI in_set_conv_decomp)
qed

lemma strict_events_of_subset_events_of : ‹α(P) ⊆ α(P)›
  by (simp add: events_of_is_strict_events_of_or_UNIV)


subsection ‹Ticks of a Process›

definition ticks_of :: ‹('a, 'r) processptick ⇒ 'r set› (‹✓s'(_')›)
  where ‹✓s(P) ≡ {r. ∃t. t @ [✓(r)] ∈ 𝒯 P}›

lemma ticks_of_memI : ‹t @ [✓(r)] ∈ 𝒯 P ⟹ r ∈ ✓s(P)›
  unfolding ticks_of_def by blast

lemma ticks_of_memD : ‹r ∈ ✓s(P) ⟹ ∃t. t @ [✓(r)] ∈ 𝒯 P›
  unfolding ticks_of_def by blast

lemma ticks_of_memE :
  ‹r ∈ ✓s(P) ⟹ (⋀t. t @ [✓(r)] ∈ 𝒯 P ⟹ thesis) ⟹ thesis›
  by (meson ticks_of_memD)


definition strict_ticks_of :: ‹('a, 'r) processptick ⇒ 'r set› (‹✓s'(_')›)
  where ‹✓s(P) ≡ {r. ∃s. s @ [✓(r)] ∈ 𝒯 P - 𝒟 P}›

lemma strict_ticks_of_memI :
  ‹t @ [✓(r)] ∈ 𝒯 P ⟹ t @ [✓(r)] ∉ 𝒟 P ⟹ r ∈ ✓s(P)›
  unfolding strict_ticks_of_def by blast

lemma strict_ticks_of_memD :
  ‹r ∈ ✓s(P) ⟹ ∃t. t @ [✓(r)] ∈ 𝒯 P ∧ t ∉ 𝒟 P›
  by (simp add: strict_ticks_of_def)
    (metis T_imp_front_tickFree butlast_snoc
      front_tickFree_iff_tickFree_butlast front_tickFree_single is_processT7)

lemma strict_ticks_of_memE :
  ‹r ∈ ✓s(P) ⟹ (⋀t. t @ [✓(r)] ∈ 𝒯 P ⟹ t ∉ 𝒟 P ⟹ thesis) ⟹ thesis›
  by (meson strict_ticks_of_memD)


lemma ticks_of_is_strict_ticks_of_or_UNIV :
  ‹✓s(P) = (if 𝒟 P = {} then ✓s(P) else UNIV)›
proof (split if_split, intro conjI impI)
  show ‹𝒟 P = {} ⟹ ✓s(P) = ✓s(P)› by (simp add: ticks_of_def strict_ticks_of_def)
next
  assume ‹𝒟 P ≠ {}›
  with nonempty_divE obtain t where ‹tF t› ‹t ∈ 𝒟 P› by blast
  hence ‹t @ [✓(r)] ∈ 𝒟 P› for r by (simp add: is_processT7)
  thus ‹✓s(P) = UNIV› by (metis D_T UNIV_eq_I ticks_of_memI)
qed

lemma strict_ticks_of_subset_ticks_of : ‹✓s(P) ⊆ ✓s(P)›
  by (simp add: ticks_of_is_strict_ticks_of_or_UNIV)



section ‹Laws›

subsection ‹Preliminaries›

lemma inj_on_map_map_eventptick_T_tickFree :
  ‹inj_on (map (map_eventptick f g)) {t ∈ 𝒯 P. tF t}› if ‹inj_on f α(P)›
proof (rule inj_onI)
  have * : ‹map_eventptick f g ∘ ev = ev ∘ f› by (rule ext) simp
  have ** : ‹map ev v ∈ 𝒯 P ⟹ map ev v' ∈ 𝒯 P ⟹
             map (ev ∘ f) v = map (ev ∘ f) v' ⟹ v = v'› for v v'
  proof (induct v arbitrary: v' rule: rev_induct)
    case Nil thus ?case by simp
  next
    case (snoc a v)
    from snoc.prems(3) obtain a' v'' where ‹v' = v'' @ [a']›
      by (metis list.map_disc_iff rev_exhaust)
    from snoc.prems(1-3) have ‹a = a'›
      by (auto simp add: ‹v' = v'' @ [a']›
          intro!: inj_onD[OF ‹inj_on f α(P)›] events_of_memI)
    from is_processT3_TR_append snoc.prems(1, 2)
    have ‹map ev v ∈ 𝒯 P› ‹map ev v'' ∈ 𝒯 P› by (simp_all add: ‹v' = v'' @ [a']›)
    with ‹a = a'› ‹v' = v'' @ [a']› snoc.hyps snoc.prems(3) show ?case
      by (metis append_same_eq map_append)
  qed

  fix t t' assume $ : ‹t ∈ {t ∈ 𝒯 P. tF t}› ‹t' ∈ {t ∈ 𝒯 P. tF t}›
    ‹map (map_eventptick f g) t = map (map_eventptick f g) t'›
  from "$"(1, 2) obtain v v' where ‹t = map ev v› ‹t' = map ev v'›
    by (auto simp add: tickFree_iff_is_map_ev)
  with "$" "*" "**" show ‹t = t'› by auto
qed


lemma inj_on_map_map_eventptick_T :
  ‹inj_on (map (map_eventptick f g)) (𝒯 P)› if ‹inj_on f α(P)› ‹inj_on g ✓s(P)›
proof (rule inj_onI)
  fix t t' assume $ : ‹t ∈ 𝒯 P› ‹t' ∈ 𝒯 P› ‹map (map_eventptick f g) t = map (map_eventptick f g) t'›
  then consider ‹tF t› ‹tF t'›
    | r r' u u' where ‹t = u @ [✓(r)]› ‹t' = u' @ [✓(r')]› ‹tF u› ‹tF u'›
      ‹map (map_eventptick f g) u = map (map_eventptick f g) u'›
    by (cases t rule: rev_cases; cases t' rule: rev_cases, simp_all)
      (metis append_T_imp_tickFree eventptick.disc(1) eventptick.exhaust eventptick.map_disc_iff(1) neq_Nil_conv)
  thus ‹t = t'›
  proof cases
    show ‹t = t'› if ‹tF t› ‹tF t'›
      by (rule inj_on_map_map_eventptick_T_tickFree
          [OF ‹inj_on f α(P)›, THEN inj_onD, OF "$"(3)])
        (simp_all add: "$"(1, 2) ‹tF t› ‹tF t'›)
  next
    fix r r' u u' assume $$ : ‹t = u @ [✓(r)]› ‹t' = u' @ [✓(r')]› ‹tF u› ‹tF u'›
      ‹map (map_eventptick f g) u = map (map_eventptick f g) u'›
    from "$$"(1, 2) "$"(1, 2) have ‹u ∈ 𝒯 P› ‹u' ∈ 𝒯 P›
      by (meson is_processT3_TR_append)+
    have ‹u = u'›
      by (rule inj_on_map_map_eventptick_T_tickFree
          [OF ‹inj_on f α(P)›, THEN inj_onD, OF "$$"(5)])
        (simp_all add: ‹u ∈ 𝒯 P› ‹u' ∈ 𝒯 P› ‹tF u› ‹tF u'›)
    moreover from "$"(1-3) "$$"(1, 2) have ‹r = r'›
      by (auto intro: inj_onD[OF ‹inj_on g ✓s(P)›] ticks_of_memI)
    ultimately show ‹t = t'› by (simp add: "$$")
  qed
qed


lemma inj_on_map_map_eventptick_T_diff_D_tickFree :
  ‹inj_on (map (map_eventptick f g)) {t ∈ 𝒯 P - 𝒟 P. tF t}› if ‹inj_on f α(P)›
proof (rule inj_onI)
  have * : ‹map_eventptick f g ∘ ev = ev ∘ f› by (rule ext) simp
  have ** : ‹⟦map ev v ∈ 𝒯 P; map ev v ∉ 𝒟 P;
             map ev v' ∈ 𝒯 P; map ev v' ∉ 𝒟 P;
             map (ev ∘ f) v = map (ev ∘ f) v'⟧ ⟹ v = v'› for v v'
  proof (induct v arbitrary: v' rule: rev_induct)
    case Nil thus ?case by simp
  next
    case (snoc a v)
    from snoc.prems(5) obtain a' v'' where ‹v' = v'' @ [a']›
      by (metis list.map_disc_iff rev_exhaust)
    from snoc.prems(1-5) have ‹a = a'›
      by (auto simp add: ‹v' = v'' @ [a']›
          intro!: inj_onD[OF ‹inj_on f α(P)›] strict_events_of_memI)
    from is_processT3_TR_append is_processT7 snoc.prems(1-4)
    have ‹map ev v ∈ 𝒯 P› ‹map ev v ∉ 𝒟 P›
      ‹map ev v'' ∈ 𝒯 P› ‹map ev v'' ∉ 𝒟 P›
      by (fastforce simp add: ‹v' = v'' @ [a']›)+
    with ‹a = a'› ‹v' = v'' @ [a']› snoc.hyps snoc.prems(5) show ?case
      by (metis append_same_eq map_append)
  qed

  fix t t' assume $ : ‹t ∈ {t ∈ 𝒯 P - 𝒟 P. tF t}› ‹t' ∈ {t ∈ 𝒯 P - 𝒟 P. tF t}›
    ‹map (map_eventptick f g) t = map (map_eventptick f g) t'›
  from "$"(1, 2) obtain v v' where ‹t = map ev v› ‹t' = map ev v'›
    by (auto simp add: tickFree_iff_is_map_ev)
  with "$" "*" "**" show ‹t = t'› by auto
qed


lemma inj_on_map_map_eventptick_T_diff_D :
  ‹inj_on (map (map_eventptick f g)) (𝒯 P - 𝒟 P)› if ‹inj_on f α(P)› and ‹inj_on g ✓s(P)›
proof (rule inj_onI)
  fix t t' assume $ : ‹t ∈ 𝒯 P - 𝒟 P› ‹t' ∈ 𝒯 P - 𝒟 P›
    ‹map (map_eventptick f g) t = map (map_eventptick f g) t'›
  then consider ‹tF t› ‹tF t'›
    | r r' u u' where ‹t = u @ [✓(r)]› ‹t' = u' @ [✓(r')]› ‹tF u› ‹tF u'›
      ‹map (map_eventptick f g) u = map (map_eventptick f g) u'›
    by (cases t rule: rev_cases; cases t' rule: rev_cases, simp_all)
      (metis append_T_imp_tickFree eventptick.disc(1) eventptick.exhaust eventptick.map_disc_iff(1) neq_Nil_conv)
  thus ‹t = t'›
  proof cases
    show ‹t = t'› if ‹tF t› ‹tF t'›
      by (rule inj_on_map_map_eventptick_T_diff_D_tickFree
          [OF ‹inj_on f α(P)›, THEN inj_onD, OF "$"(3)])
        (use "$"(1, 2) in ‹simp_all add: ‹tF t› ‹tF t'››)
  next
    fix r r' u u' assume $$ : ‹t = u @ [✓(r)]› ‹t' = u' @ [✓(r')]› ‹tF u› ‹tF u'›
      ‹map (map_eventptick f g) u = map (map_eventptick f g) u'›
    from "$$"(1-4) "$"(1, 2) have ‹u ∈ 𝒯 P› ‹u ∉ 𝒟 P› ‹u' ∈ 𝒯 P› ‹u' ∉ 𝒟 P›
      by (auto intro: is_processT3_TR_append is_processT7)
    have ‹u = u'›
      by (rule inj_on_map_map_eventptick_T_diff_D_tickFree
          [OF ‹inj_on f α(P)›, THEN inj_onD, OF "$$"(5)])
        (simp_all add: ‹u ∈ 𝒯 P› ‹u ∉ 𝒟 P› ‹u' ∈ 𝒯 P› ‹u' ∉ 𝒟 P› ‹tF u› ‹tF u'›)
    moreover from "$"(1-3) "$$"(1, 2) have ‹r = r'›
      by (auto intro: inj_onD[OF ‹inj_on g ✓s(P)›] strict_ticks_of_memI)
    ultimately show ‹t = t'› by (simp add: "$$")
  qed
qed


subsection ‹Events of a Process›

lemma events_of_BOT  [simp] : ‹α(⊥) = UNIV›
  and events_of_SKIP [simp] : ‹α(SKIP r) = {}›
  and events_of_STOP [simp] : ‹α(STOP) = {}›
  by (auto simp add: events_of_def T_BOT T_SKIP T_STOP)
    (meson front_tickFree_single list.set_intros(1))

lemma anti_mono_events_of_T: ‹P ⊑T Q ⟹ α(Q) ⊆ α(P)›
  unfolding trace_refine_def events_of_def by blast

lemma anti_mono_events_of_F: ‹P ⊑F Q ⟹ α(Q) ⊆ α(P)›
  by (intro anti_mono_events_of_T leF_imp_leT)

lemma anti_mono_events_of_FD: ‹P ⊑FD Q ⟹ α(Q) ⊆ α(P)›
  by (intro anti_mono_events_of_F leFD_imp_leF)

lemma anti_mono_events_of_DT: ‹P ⊑DT Q ⟹ α(Q) ⊆ α(P)›
  by (intro anti_mono_events_of_T leDT_imp_leT)

lemma anti_mono_events_of : ‹P ⊑ Q ⟹ α(Q) ⊆ α(P)›
  by (intro anti_mono_events_of_FD le_approx_imp_le_ref)



lemma events_of_GlobalNdet: ‹α(⊓a ∈ A. P a) = (⋃a∈A. α(P a))›
  by (simp add: events_of_def T_GlobalNdet)


lemma events_of_write0 : ‹α(a → P) = insert a α(P)›
  by (fastforce simp add: events_of_def write0_def T_Mprefix)

lemma events_of_Mndetprefix: ‹α(⊓a∈A → P a) = A ∪ (⋃a∈A. α(P a))›
  by (auto simp add: Mndetprefix_GlobalNdet events_of_GlobalNdet events_of_write0)

lemma events_of_Mprefix: ‹α(□a∈A → P a) = A ∪ (⋃a∈A. α(P a))›
  by (simp add: events_of_def write0_def T_Mprefix set_eq_iff)
    (metis eventptick.inject(1) is_processT1_TR list.set_intros set_ConsD)


lemma events_of_read :
  ‹α(c?a∈A → P a) = c ` A ∪ (⋃a∈c ` A. α(P (inv_into A c a)))›
  by (simp add: read_def events_of_Mprefix)

lemma events_of_inj_on_read :
  ‹inj_on c A ⟹ α(c?a∈A → P a) = c ` A ∪ (⋃a∈A. α(P a))›
  by (simp add: events_of_read)

lemma events_of_ndet_write :
  ‹α(c!!a∈A → P a) = c ` A ∪ (⋃a∈c ` A. α(P (inv_into A c a)))›
  by (simp add: ndet_write_def events_of_Mndetprefix)

lemma events_of_inj_on_ndet_write :
  ‹inj_on c A ⟹ α(c!!a∈A → P a) = c ` A ∪ (⋃a∈A. α(P a))›
  by (simp add: events_of_ndet_write)

lemma events_of_write : ‹α(c!a → P) = insert (c a) α(P)›
  by (simp add: write_def events_of_Mprefix)



lemma events_of_Ndet: ‹α(P ⊓ Q) = α(P) ∪ α(Q)›
  unfolding events_of_def by (simp add: T_Ndet)

lemma events_of_Det: ‹α(P □ Q) = α(P) ∪ α(Q)›
  unfolding events_of_def by (simp add: T_Det)

lemma events_of_Sliding: ‹α(P ⊳ Q) = α(P) ∪ α(Q)›
  unfolding Sliding_def by (simp add: events_of_Ndet events_of_Det)


lemma events_of_Renaming:
  ‹α(Renaming P f g) = (if 𝒟 P = {} then f ` α(P) else UNIV)›
proof (simp, intro conjI impI)
  show ‹𝒟 P ≠ {} ⟹ α(Renaming P f g) = UNIV›
    by (simp add: events_of_is_strict_events_of_or_UNIV D_Renaming)
      (metis front_tickFree_Nil nonempty_divE)
next
  show ‹𝒟 P = {} ⟹ α(Renaming P f g) = f ` α(P)›
    by (auto simp add: events_of_def T_Renaming image_UN image_iff eventptick.case_eq_if)
      (metis eventptick.inject(1) eventptick.map_disc_iff(1) eventptick.simps(9) is_ev_def,
        metis (mono_tags, lifting) eventptick.simps(9) image_iff list.set_map)
qed


lemma events_of_Seq : ‹α(P ; Q) = α(P) ∪ (if ✓s(P) = {} then {} else α(Q))› (is ‹_ = ?A›)
proof (intro subset_antisym subsetI)
  show ‹a ∈ α(P ; Q) ⟹ a ∈ ?A› for a
  proof (elim events_of_memE, unfold T_Seq, elim UnE disjE conjE exE)
    show ‹ev a ∈ set t ⟹ t ∈ {t ∈ 𝒯 P. tF t} ⟹ a ∈ ?A› for t
      by (auto intro: events_of_memI)
  next
    show ‹ev a ∈ set t ⟹ t ∈ {t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ u ∈ 𝒯 Q} ⟹ a ∈ ?A› for t
      by simp (metis UNIV_I UnE UnI1 empty_iff events_of_is_strict_events_of_or_UNIV
          events_of_memI set_append strict_ticks_of_memI)
  next
    show ‹ev a ∈ set t ⟹ t ∈ 𝒟 P ⟹ a ∈ ?A› for t
      by simp (metis UNIV_I empty_iff events_of_is_strict_events_of_or_UNIV)
  qed
next
  show ‹a ∈ ?A ⟹ a ∈ α(P ; Q)› for a
    by (elim UnE events_of_memE, simp_all add: events_of_def T_Seq split: if_split_asm)
      (metis T_nonTickFree_imp_decomp Un_iff eventptick.distinct(1) is_processT1_TR set_ConsD set_append,
        metis Un_iff ex_in_conv set_append strict_ticks_of_memD)
qed



lemma events_of_Sync_subset : ‹α(P ⟦S⟧ Q) ⊆ α(P) ∪ α(Q)›
  by (subst events_of_def, simp add: T_Sync subset_iff)
    (metis UNIV_I empty_iff events_of_is_strict_events_of_or_UNIV events_of_memI ftf_Sync1)


lemma events_of_Inter: ‹α((P :: ('a, 'r) processptick) ||| Q) = α(P) ∪ α(Q)›
proof (rule subset_antisym[OF events_of_Sync_subset])
  have ‹α(P :: ('a, 'r) processptick) ⊆ α(P ||| Q)› for P Q
  proof (auto simp add: events_of_def T_Sync, goal_cases)
    case (1 e t_P)
    show ?case 
    proof (cases ‹tF t_P›)
      case True
      thus ?thesis 
        by (metis "1"(1) "1"(3) emptyLeftSelf insert_absorb insert_disjoint(2)
            is_processT1_TR setinterleaving_sym tickFree_def)
    next
      case False
      then obtain t_P' r where ‹t_P = t_P' @ [✓(r)]› ‹tF t_P'› ‹t_P' ∈ 𝒯 P›
        by (metis "1"(1) prefixI T_nonTickFree_imp_decomp
            append_T_imp_tickFree is_processT3_TR not_Cons_self)
      moreover have ‹ev e ∈ set t_P'›
        using "1"(3) calculation(1) by auto
      ultimately show ?thesis
        apply (rule_tac x = t_P' in exI, simp)
        apply (rule_tac x = t_P' in exI, simp)
        apply (rule_tac x = ‹[]› in exI, simp)
        by (metis disjoint_iff emptyLeftSelf setinterleaving_sym tickFree_def)
    qed
  qed
  thus ‹α(P) ∪ α(Q) ⊆ α(P ||| Q)› by (metis Sync_commute Un_least)
qed



lemma events_of_Par_div    :
  ‹𝒟 P ∩ 𝒯 Q ∪ 𝒟 Q ∩ 𝒯 P ≠ {} ⟹ α(P || Q) = UNIV›
  and events_of_Par_subset :
  ‹𝒟 P ∩ 𝒯 Q ∪ 𝒟 Q ∩ 𝒯 P = {} ⟹ α(P || Q) ⊆ α(P) ∩ α(Q)›
proof -
  assume ‹𝒟 P ∩ 𝒯 Q ∪ 𝒟 Q ∩ 𝒯 P ≠ {}›
  hence ‹𝒟 (P || Q) ≠ {}› by (simp add: D_Sync setinterleaving_UNIV_iff)
      (use front_tickFree_Nil in blast)
  thus ‹α(P || Q) = UNIV› by (simp add: events_of_is_strict_events_of_or_UNIV)
next
  show ‹𝒟 P ∩ 𝒯 Q ∪ 𝒟 Q ∩ 𝒯 P = {} ⟹ α(P || Q) ⊆ α(P) ∩ α(Q)›
    by (auto simp add: events_of_def T_Par)
qed


lemma events_of_Hiding:
  ‹α(P \ B) = (if 𝒟 (P \ B) = {} then α(P) - B else UNIV)›
proof (split if_split, intro conjI impI)
  show ‹𝒟 (P \ B) ≠ {} ⟹ α(P \ B) = UNIV›
    by (simp add: events_of_is_strict_events_of_or_UNIV)
next
  show ‹α(P \ B) = α(P) - B› if ‹𝒟 (P \ B) = {}›
  proof (intro subset_antisym subsetI)
    from ‹𝒟 (P \ B) = {}› have ‹div_hide P B = {}› unfolding D_Hiding by blast
    fix a assume ‹a ∈ α(P \ B)›
    then obtain t where ‹ev a ∈ set (trace_hide t (ev ` B))› ‹(t, ev ` B) ∈ ℱ P›
      by (elim events_of_memE, unfold T_Hiding ‹div_hide P B = {}›, blast)
    thus ‹a ∈ α(P) - B› by (metis DiffI F_T events_of_memI
          filter_set image_eqI member_filter)
  next
    fix a assume ‹a ∈ α(P) - B›
    then obtain t where ‹ev a ∈ set t› ‹t ∈ 𝒯 P› ‹a ∉ B›
      by (metis DiffE events_of_memD)
    hence ‹ev a ∈ set (trace_hide t (ev ` B))› ‹trace_hide t (ev ` B) ∈ 𝒯 (P \ B)›
      by (auto intro: mem_T_imp_mem_T_Hiding)
    thus ‹a ∈ events_of (P \ B)› by (simp add: events_of_memI)
  qed
qed


subsection ‹Strict Events of a Process›

lemma strict_events_of_BOT  [simp] : ‹α(⊥) = {}›
  and strict_events_of_SKIP [simp] : ‹α(SKIP r) = {}›
  and strict_events_of_STOP [simp] : ‹α(STOP) = {}›
  by (auto simp add: strict_events_of_def T_BOT T_SKIP T_STOP D_BOT)


lemma strict_events_of_GlobalNdet_subset : ‹α(⊓a ∈ A. P a) ⊆ (⋃a∈A. α(P a))›
  by (auto simp add: strict_events_of_def GlobalNdet_projs)


lemma strict_events_of_Mprefix:
  ‹α(□a∈A → P a) = {a∈A. P a ≠ ⊥} ∪ (⋃a∈{a∈A. P a ≠ ⊥}. α(P a))›
proof -
  have ‹(⋃a∈{a∈A. P a ≠ ⊥}. α(P a)) = (⋃a∈A. α(P a))› by auto
  show ‹α(□a∈A → P a) = {a∈A. P a ≠ ⊥} ∪ (⋃a∈{a∈A. P a ≠ ⊥}. α(P a))›
  proof (unfold ‹?this›, safe)
    show ‹a ∈ α(□a∈A → P a) ⟹ a ∉ (⋃a∈A. α(P a)) ⟹ a ∈ A› for a
      by (auto simp add: strict_events_of_def Mprefix_projs) blast
  next
    show ‹a ∈ α(□a∈A → P a) ⟹ a ∉ (⋃a∈A. α(P a)) ⟹ P a = ⊥ ⟹ False› for a
      by (auto simp add: strict_events_of_def Mprefix_projs BOT_projs) blast
  next
    fix a assume ‹a ∈ A› ‹P a ≠ ⊥›
    hence * : ‹∃t∈insert [] {ev a # s |a s. a ∈ A ∧ s ∈ 𝒯 (P a)} -
                  {ev a # s |a s. a ∈ A ∧ s ∈ 𝒟 (P a)}. ev a ∈ set t›
      by (intro bexI[where x = ‹[ev a]›]) (simp_all add: BOT_iff_Nil_D)
    show ‹a ∈ α(□a∈A → P a)›
      by (auto simp add: strict_events_of_def Mprefix_projs intro: "*")
  next
    fix a b assume ‹a ∈ A› ‹b ∈ α(P a)›
    then obtain t where ‹t ∈ 𝒯 (P a)› ‹t ∉ 𝒟 (P a)› ‹ev b ∈ set t›
      by (meson strict_events_of_memE)
    hence * : ‹∃u∈insert [] {ev a # s |a s. a ∈ A ∧ s ∈ 𝒯 (P a)} -
                  {ev a # s |a s. a ∈ A ∧ s ∈ 𝒟 (P a)}. ev b ∈ set u›
      by (intro bexI[where x = ‹ev a # t›]) (simp_all add: ‹a ∈ A›)
    show ‹b ∈ α(□a∈A → P a)›
      by (auto simp add: strict_events_of_def Mprefix_projs intro: "*")
  qed
qed

lemma strict_events_of_Mndetprefix:
  ‹α(⊓a∈A → P a) = {a∈A. P a ≠ ⊥} ∪ (⋃a∈{a∈A. P a ≠ ⊥}. α(P a))›
proof -
  have ‹𝒯 (⊓a∈A → P a) = 𝒯 (□a∈A → P a)› by (simp add: T_Mndetprefix' T_Mprefix)
  moreover have ‹𝒟 (⊓a∈A → P a) = 𝒟 (□a∈A → P a)› by (simp add: D_Mndetprefix' D_Mprefix)
  ultimately have ‹α(⊓a∈A → P a) = α(□a∈A → P a)› by (simp add: strict_events_of_def)
  thus ‹α(⊓a∈A → P a) = {a∈A. P a ≠ ⊥} ∪ (⋃a∈{a∈A. P a ≠ ⊥}. α(P a))›
    by (simp add: strict_events_of_Mprefix)
qed

lemma strict_events_of_write0 : ‹α(a → P) = (if P = ⊥ then {} else insert a α(P))›
  by (simp add: write0_def strict_events_of_Mprefix)

lemma strict_events_of_read :
  ‹α(c?a∈A → P a) = {c a |a. a ∈ A ∧ P (inv_into A c (c a)) ≠ ⊥} ∪
                      (⋃a∈{a ∈ A. P (inv_into A c (c a)) ≠ ⊥}. α(P (inv_into A c (c a))))›
  by (auto simp add: read_def strict_events_of_Mprefix)

lemma strict_events_of_inj_on_read :
  ‹inj_on c A ⟹ α(c?a∈A → P a) = {c a |a. a ∈ A ∧ P a ≠ ⊥} ∪
                                    (⋃a∈{a ∈ A. P a ≠ ⊥}. α(P a))›
  by (auto simp add: strict_events_of_read)

lemma strict_events_of_ndet_write :
  ‹α(c!!a∈A → P a) = {c a |a. a ∈ A ∧ P (inv_into A c (c a)) ≠ ⊥} ∪
                       (⋃a∈{a ∈ A. P (inv_into A c (c a)) ≠ ⊥}. α(P (inv_into A c (c a))))›
  by (auto simp add: ndet_write_def strict_events_of_Mndetprefix)

lemma strict_events_of_inj_on_ndet_write :
  ‹inj_on c A ⟹ α(c!!a∈A → P a) = {c a |a. a ∈ A ∧ P a ≠ ⊥} ∪
                                      (⋃a∈{a ∈ A. P a ≠ ⊥}. α(P a))›
  by (auto simp add: strict_events_of_ndet_write)

lemma strict_events_of_write : ‹α(c!a → P) = (if P = ⊥ then {} else insert (c a) α(P))›
  by (simp add: write_def strict_events_of_Mprefix)



lemma strict_events_of_Ndet_subset : ‹α(P ⊓ Q) ⊆ α(P) ∪ α(Q)›
  unfolding strict_events_of_def by (auto simp add: Ndet_projs)

lemma strict_events_of_Det_subset : ‹α(P □ Q) ⊆ α(P) ∪ α(Q)›
  unfolding strict_events_of_def by (auto simp add: Det_projs)

lemma strict_events_of_Sliding_subset : ‹α(P ⊳ Q) ⊆ α(P) ∪ α(Q)›
  unfolding strict_events_of_def by (auto simp add: Sliding_projs)


lemma strict_events_of_Renaming_subset : ‹α(Renaming P f g) ⊆ f ` α(P)›
proof (intro subsetI)
  show ‹b ∈ α(Renaming P f g) ⟹ b ∈ f ` α(P)› for b
  proof (elim strict_events_of_memE)
    fix u assume ‹u ∈ 𝒯 (Renaming P f g)› ‹u ∉ 𝒟 (Renaming P f g)› ‹ev b ∈ set u›
    then obtain u' where ‹tF u'› ‹u' ∈ 𝒯 (Renaming P f g)› ‹u' ∉ 𝒟 (Renaming P f g)› ‹ev b ∈ set u'›
      by (cases u rule: rev_cases, simp_all)
        (metis prefixI ‹ev b ∈ set u› append_T_imp_tickFree eventptick.disc(1) front_tickFree_single
          is_processT3_TR is_processT7 not_Cons_self2 tickFree_Cons_iff tickFree_Nil tickFree_append_iff)
    from this(1-3) front_tickFree_Nil map_eventptick_tickFree obtain t
      where ‹u' = map (map_eventptick f g) t› ‹t ∈ 𝒯 P› ‹t ∉ 𝒟 P› unfolding Renaming_projs by blast
    from this(1) ‹ev b ∈ set u'› obtain a where ‹b = f a› ‹ev a ∈ set t›
      by (auto simp add: in_set_conv_decomp)
        (metis eventptick.map_disc_iff(1) eventptick.map_sel(1) eventptick.sel(1) is_ev_def)
    with ‹t ∈ 𝒯 P› ‹t ∉ 𝒟 P› show ‹b ∈ f ` α(P)› by (auto intro: strict_events_of_memI)
  qed
qed


lemma strict_events_of_inj_on_Renaming :
  ‹α(Renaming P f g) = f ` α(P)› if ‹inj_on f α(P)›
proof (rule subset_antisym)
  show ‹α(Renaming P f g) ⊆ f ` α(P)› by (fact strict_events_of_Renaming_subset)
next
  show ‹f ` α(P) ⊆ α(Renaming P f g)›
  proof (rule subsetI, elim imageE strict_events_of_memE)
    fix b a t assume ‹b = f a› ‹t ∈ 𝒯 P› ‹t ∉ 𝒟 P› ‹ev a ∈ set t›
    from ‹t ∈ 𝒯 P› ‹t ∉ 𝒟 P› ‹ev a ∈ set t› obtain t'
      where ‹tF t'› ‹t' ∈ 𝒯 P› ‹t' ∉ 𝒟 P› ‹ev a ∈ set t'›
      by (cases t rule: rev_cases, simp_all)
        (metis prefixI ‹ev a ∈ set t› append_T_imp_tickFree eventptick.disc(1) front_tickFree_single
          is_processT3_TR is_processT7 not_Cons_self2 tickFree_Cons_iff tickFree_Nil tickFree_append_iff)
    from ‹t' ∈ 𝒯 P› have ‹map (map_eventptick f g) t' ∈ 𝒯 (Renaming P f g)›
      by (auto simp add: T_Renaming)
    have ‹map (map_eventptick f g) t' ∉ 𝒟 (Renaming P f g)›
    proof (rule ccontr)
      assume ‹¬ map (map_eventptick f g) t' ∉ 𝒟 (Renaming P f g)›
      then obtain u1 u2 where * : ‹ftF u2› ‹tF u1› ‹u1 ∈ 𝒟 P›
        ‹map (map_eventptick f g) t' = map (map_eventptick f g) u1 @ u2›
        unfolding D_Renaming by blast
      from this(4) obtain t1 t2
        where ** : ‹t' = t1 @ t2› ‹map (map_eventptick f g) t2 = u2›
          ‹map (map_eventptick f g) t1 = map (map_eventptick f g) u1›
        by (metis (no_types) append_eq_map_conv)
      from "**"(1) ‹t' ∈ 𝒯 P› ‹tF t'› is_processT3_TR_append tickFree_append_iff
      have ‹t1 ∈ {t ∈ 𝒯 P. tF t}› by auto
      moreover have ‹u1 ∈ {t ∈ 𝒯 P. tF t}› by (simp add: D_T ‹tF u1› ‹u1 ∈ 𝒟 P›)
      ultimately have ‹t1 = u1› by (intro inj_on_map_map_eventptick_T_tickFree
            [THEN inj_onD, OF ‹inj_on f α(P)› "**"(3)])
      with "*"(1-3) "**"(1, 2) ‹t' ∉ 𝒟 P› is_processT7
        map_eventptick_front_tickFree show False by blast
    qed
    moreover from ‹ev a ∈ set t'› ‹b = f a› have ‹ev b ∈ set (map (map_eventptick f g) t')› by force
    ultimately show ‹b ∈ α(Renaming P f g)›
      using ‹map (map_eventptick f g) t' ∈ 𝒯 (Renaming P f g)› by (auto intro: strict_events_of_memI)
  qed
qed



lemma strict_events_of_Seq_subseteq :
  ‹α(P ; Q) ⊆ α(P) ∪ (if ✓s(P) = {} then {} else α(Q))›
  by (rule subsetI, elim strict_events_of_memE, simp add: Seq_projs)
    (metis T_imp_front_tickFree Un_iff append_T_imp_tickFree empty_iff is_processT7
      is_processT9 not_Cons_self2 set_append strict_events_of_memI strict_ticks_of_memI)


lemma strict_events_of_Sync_subset : ‹α(P ⟦S⟧ Q) ⊆ α(P) ∪ α(Q)›
  by (subst strict_events_of_def, auto simp add: Sync_projs subset_iff)
    (metis (full_types) append_Nil2 front_tickFree_Nil ftf_Sync1
      setinterleaving_sym strict_events_of_memI)





section ‹Ticks of a Process›

lemma ticks_of_BOT  [simp] : ‹✓s(⊥) = UNIV›
  and ticks_of_SKIP [simp] : ‹✓s(SKIP r) = {r}›
  and ticks_of_STOP [simp] : ‹✓s(STOP) = {}›
  by (simp_all add: set_eq_iff ticks_of_def T_BOT T_SKIP T_STOP)
    (metis append_Nil front_tickFree_single)

lemma anti_mono_ticks_of_T: ‹P ⊑T Q ⟹ ✓s(Q) ⊆ ✓s(P)›
  unfolding trace_refine_def ticks_of_def by blast

lemma anti_mono_ticks_of_F: ‹P ⊑F Q ⟹ ✓s(Q) ⊆ ✓s(P)›
  by (intro anti_mono_ticks_of_T leF_imp_leT)

lemma anti_mono_ticks_of_FD: ‹P ⊑FD Q ⟹ ✓s(Q) ⊆ ✓s(P)›
  by (intro anti_mono_ticks_of_F leFD_imp_leF)

lemma anti_mono_ticks_of_DT: ‹P ⊑DT Q ⟹ ✓s(Q) ⊆ ✓s(P)›
  by (intro anti_mono_ticks_of_T leDT_imp_leT)

lemma anti_mono_ticks_of : ‹P ⊑ Q ⟹ ✓s(Q) ⊆ ✓s(P)›
  by (intro anti_mono_ticks_of_FD le_approx_imp_le_ref)



lemma ticks_of_GlobalNdet: ‹✓s(⊓a ∈ A. P a) = (⋃a∈A. ✓s(P a))›
  by (auto simp add: ticks_of_def T_GlobalNdet)


lemma ticks_of_Mprefix: ‹✓s(□a∈A → P a) = (⋃a∈A. ✓s(P a))›
  by (auto simp add: set_eq_iff ticks_of_def T_Mprefix)
    (metis append_butlast_last_id eventptick.distinct(1) last.simps last_snoc, meson append_Cons)

lemma ticks_of_write0 : ‹✓s(a → P) = ✓s(P)›
  by (simp add: write0_def ticks_of_Mprefix)

lemma ticks_of_Mndetprefix: ‹✓s(⊓a∈A → P a) = (⋃a∈A. ✓s(P a))›
  by (simp add: Mndetprefix_GlobalNdet ticks_of_GlobalNdet ticks_of_write0)



lemma ticks_of_read :
  ‹✓s(c?a∈A → P a) = (⋃a∈c ` A. ✓s(P (inv_into A c a)))›
  by (simp add: read_def ticks_of_Mprefix)

lemma ticks_of_inj_on_read :
  ‹inj_on c A ⟹ ✓s(c?a∈A → P a) = (⋃a∈A. ✓s(P a))›
  by (simp add: ticks_of_read)

lemma ticks_of_ndet_write :
  ‹✓s(c!!a∈A → P a) = (⋃a∈c ` A. ✓s(P (inv_into A c a)))›
  by (simp add: ndet_write_def ticks_of_Mndetprefix)

lemma ticks_of_inj_on_ndet_write :
  ‹inj_on c A ⟹ ✓s(c!!a∈A → P a) = (⋃a∈A. ✓s(P a))›
  by (simp add: ticks_of_ndet_write)

lemma ticks_of_write : ‹✓s(c!a → P) = ✓s(P)›
  by (simp add: write_def ticks_of_Mprefix)



lemma ticks_of_Ndet: ‹✓s(P ⊓ Q) = ✓s(P) ∪ ✓s(Q)›
  by (auto simp add: ticks_of_def T_Ndet)

lemma ticks_of_Det: ‹✓s(P □ Q) = ✓s(P) ∪ ✓s(Q)›
  by (auto simp add: ticks_of_def T_Det)

lemma ticks_of_Sliding: ‹✓s(P ⊳ Q) = ✓s(P) ∪ ✓s(Q)›
  by (auto simp add: ticks_of_def T_Sliding)


lemma ticks_of_Renaming:
  ‹✓s(Renaming P f g) = (if 𝒟 P = {} then g ` ✓s(P) else UNIV)›
proof (simp, intro conjI impI)
  show ‹𝒟 P ≠ {} ⟹ ✓s(Renaming P f g) = UNIV›
    by (simp add: ticks_of_is_strict_ticks_of_or_UNIV D_Renaming)
      (meson front_tickFree_Nil nonempty_divE)
next
  show ‹✓s(Renaming P f g) = g ` ✓s(P)› if ‹𝒟 P = {}›
  proof (intro subset_antisym subsetI)
    show ‹r ∈ ✓s(Renaming P f g) ⟹ r ∈ g ` ✓s(P)› for r
      by (auto simp add: T_Renaming ‹𝒟 P = {}› append_eq_map_conv tick_eq_map_map_eventptick_iff
          intro!: ticks_of_memI elim!: ticks_of_memE)
  next
    show ‹r ∈ g ` ✓s(P) ⟹ r ∈ ✓s(Renaming P f g)› for r
      by (simp add: ticks_of_def T_Renaming ‹𝒟 P = {}›
          append_eq_map_conv tick_eq_map_map_eventptick_iff) blast
  qed
qed


lemma ticks_of_Seq :
  ‹✓s(P ; Q) = (if 𝒟 P = {} then if ✓s(P) = {} then {} else ✓s(Q) else UNIV)› (is ‹?lhs = ?rhs›)
proof (intro subset_antisym subsetI)
  show ‹a ∈ ?lhs ⟹ a ∈ ?rhs› for a
    by (elim ticks_of_memE, auto simp add: T_Seq ticks_of_def)
      (metis T_nonTickFree_imp_decomp append_T_imp_tickFree last_appendR
        last_snoc non_tickFree_tick tickFree_Nil tickFree_append_iff)
next
  show ‹a ∈ ?rhs ⟹ a ∈ ?lhs› for a
    by (auto simp add: ticks_of_def T_Seq split: if_split_asm)
      (meson append_assoc, metis all_not_in_conv front_tickFree_single is_processT7 nonempty_divE)
qed


lemma ticks_of_Sync_subset : ‹✓s(P ⟦S⟧ Q) ⊆ ✓s(P) ∪ ✓s(Q)›
  by (auto simp add: T_Sync elim!: ticks_of_memE)
    (metis SyncWithTick_imp_NTF T_imp_front_tickFree ticks_of_memI,
      (metis UNIV_I empty_iff ticks_of_is_strict_ticks_of_or_UNIV)+)

lemma ticks_of_no_div_Sync_subset :
  ‹✓s(P ⟦S⟧ Q) ⊆ ✓s(P) ∩ ✓s(Q)› if ‹𝒟 (P ⟦S⟧ Q) = {}›
proof (rule subsetI)
  fix r assume ‹r ∈ ✓s(P ⟦S⟧ Q)›
  with ‹𝒟 (P ⟦S⟧ Q) = {}› obtain t t_P t_Q
    where * : ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
      ‹(t @ [✓(r)]) setinterleaves ((t_P, t_Q), range tick ∪ ev ` S)›
    by (elim ticks_of_memE, unfold Sync_projs, blast)
  from SyncWithTick_imp_NTF[OF "*"(3) "*"(1, 2)[THEN is_processT2_TR]]
  obtain t_P' t_Q' where ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(r)]› by blast
  with "*"(1, 2) show ‹r ∈ ✓s(P) ∩ ✓s(Q)› by (auto intro: ticks_of_memI)
qed

lemma ticks_of_Par_div :
  ‹𝒟 P ∩ 𝒯 Q ∪ 𝒟 Q ∩ 𝒯 P ≠ {} ⟹ ✓s(P || Q) = UNIV›
  and ticks_of_no_div_Par_subset :
  ‹𝒟 P ∩ 𝒯 Q ∪ 𝒟 Q ∩ 𝒯 P = {} ⟹ ✓s(P || Q) ⊆ ✓s(P) ∩ ✓s(Q)›
proof -
  assume ‹𝒟 P ∩ 𝒯 Q ∪ 𝒟 Q ∩ 𝒯 P ≠ {}›
  hence ‹𝒟 (P || Q) ≠ {}› by (simp add: D_Sync setinterleaving_UNIV_iff)
      (use front_tickFree_Nil in blast)
  thus ‹✓s(P || Q) = UNIV› by (simp add: ticks_of_is_strict_ticks_of_or_UNIV)
next
  show ‹𝒟 P ∩ 𝒯 Q ∪ 𝒟 Q ∩ 𝒯 P = {} ⟹ ✓s(P || Q) ⊆ ✓s(P) ∩ ✓s(Q)›
    by (rule ticks_of_no_div_Sync_subset) (auto simp add: D_Par)
qed





lemma ticks_of_Hiding:
  ‹✓s(P \ B) = (if 𝒟 (P \ B) = {} then ✓s(P) else UNIV)›
proof (split if_split, intro conjI impI)
  show ‹𝒟 (P \ B) ≠ {} ⟹ ✓s(P \ B) = UNIV›
    by (simp add: ticks_of_is_strict_ticks_of_or_UNIV)
next
  show ‹✓s(P \ B) = ✓s(P)› if ‹𝒟 (P \ B) = {}›
  proof (intro subset_antisym subsetI)
    fix r assume ‹r ∈ ✓s(P \ B)›
    then obtain u where ‹u @ [✓(r)] ∈ 𝒯 (P \ B)› by (meson ticks_of_memE)
    with ‹𝒟 (P \ B) = {}› obtain t
      where ‹u @ [✓(r)] = trace_hide t (ev ` B)› ‹(t, ev ` B) ∈ ℱ P›
      unfolding T_Hiding D_Hiding by blast
    then obtain t' where ‹t' @ [✓(r)] ∈ 𝒯 P›
      by (cases t rule: rev_cases, auto split: if_split_asm intro: F_T)
        (metis F_T Hiding_tickFree append_T_imp_tickFree list.distinct(1)
          non_tickFree_tick tickFree_append_iff)
    thus ‹r ∈ ✓s(P)› by (simp add: ticks_of_memI)
  next
    fix r assume ‹r ∈ ✓s(P)›
    then obtain t where ‹t @ [✓(r)] ∈ 𝒯 P› by (metis ticks_of_memD)
    hence ‹trace_hide (t @ [✓(r)]) (ev ` B) ∈ 𝒯 (P \ B)›
      by (fact mem_T_imp_mem_T_Hiding)
    thus ‹r ∈ ✓s(P \ B)› by (auto intro: ticks_of_memI split: if_split_asm)
  qed
qed



lemma tickFree_traces_iff_empty_ticks_of : ‹(∀t ∈ 𝒯 P. tF t) ⟷ ✓s(P) = {}›
  using T_nonTickFree_imp_decomp unfolding ticks_of_def by auto



subsection ‹Strict Events of a Process›

lemma strict_ticks_of_BOT  [simp] : ‹✓s(⊥) = {}›
  and strict_ticks_of_SKIP [simp] : ‹✓s(SKIP r) = {r}›
  and strict_ticks_of_STOP [simp] : ‹✓s(STOP) = {}›
  by (auto simp add: strict_ticks_of_def BOT_projs SKIP_projs T_STOP)


lemma strict_ticks_of_GlobalNdet_subset : ‹✓s(⊓a ∈ A. P a) ⊆ (⋃a∈A. ✓s(P a))›
  by (auto simp add: strict_ticks_of_def GlobalNdet_projs)


lemma strict_ticks_of_Mprefix:
  ‹✓s(□a∈A → P a) = (⋃a∈{a∈A. P a ≠ ⊥}. ✓s(P a))›
proof -
  have ‹(⋃a∈{a∈A. P a ≠ ⊥}. ✓s(P a)) = (⋃a∈A. ✓s(P a))›
    by (auto intro: strict_ticks_of_memI is_processT9 elim!: strict_ticks_of_memE)
      (metis D_BOT T_BOT is_processT9 strict_ticks_of_memI)
  show ‹✓s(□a∈A → P a) = (⋃a∈{a∈A. P a ≠ ⊥}. ✓s(P a))›
  proof (unfold ‹?this›, safe elim!: strict_ticks_of_memE)
    show ‹t @ [✓(r)] ∈ 𝒯 (□a∈A → P a) ⟹ t ∉ 𝒟 (□a∈A → P a)
          ⟹ r ∈ (⋃a∈A. ✓s(P a))› for t r
      by (auto simp add: strict_ticks_of_def Mprefix_projs)
        (metis append_butlast_last_id butlast.simps(2) butlast_snoc
          eventptick.distinct(1) is_processT9 last.simps last_snoc)
  next
    fix a t r assume ‹a ∈ A› ‹t @ [✓(r)] ∈ 𝒯 (P a)› ‹t ∉ 𝒟 (P a)›
    hence ‹(ev a # t) @ [✓(r)] ∈ 𝒯 (□a∈A → P a)›
      ‹(ev a # t) ∉ 𝒟 (□a∈A → P a)›
      by (auto simp add: strict_ticks_of_def Mprefix_projs)
    thus ‹r ∈ ✓s(□a∈A → P a)› by (meson strict_ticks_of_memI is_processT9)
  qed
qed

lemma strict_ticks_of_Mndetprefix:
  ‹✓s(⊓a∈A → P a) = (⋃a∈{a∈A. P a ≠ ⊥}. ✓s(P a))›
proof -
  have ‹𝒯 (⊓a∈A → P a) = 𝒯 (□a∈A → P a)› by (simp add: T_Mndetprefix' T_Mprefix)
  moreover have ‹𝒟 (⊓a∈A → P a) = 𝒟 (□a∈A → P a)› by (simp add: D_Mndetprefix' D_Mprefix)
  ultimately have ‹✓s(⊓a∈A → P a) = ✓s(□a∈A → P a)› by (simp add: strict_ticks_of_def)
  thus ‹✓s(⊓a∈A → P a) = (⋃a∈{a∈A. P a ≠ ⊥}. ✓s(P a))› by (simp add: strict_ticks_of_Mprefix)
qed

lemma strict_ticks_of_write0 : ‹✓s(a → P) = (if P = ⊥ then {} else ✓s(P))›
  by (simp add: write0_def strict_ticks_of_Mprefix)

lemma strict_ticks_of_read :
  ‹✓s(c?a∈A → P a) = (⋃a∈{a ∈ A. P (inv_into A c (c a)) ≠ ⊥}. ✓s(P (inv_into A c (c a))))›
  by (auto simp add: read_def strict_ticks_of_Mprefix)

lemma strict_ticks_of_inj_on_read :
  ‹inj_on c A ⟹ ✓s(c?a∈A → P a) = (⋃a∈{a ∈ A. P a ≠ ⊥}. ✓s(P a))›
  by (auto simp add: strict_ticks_of_read)

lemma strict_ticks_of_ndet_write :
  ‹✓s(c!!a∈A → P a) = (⋃a∈{a ∈ A. P (inv_into A c (c a)) ≠ ⊥}. ✓s(P (inv_into A c (c a))))›
  by (auto simp add: ndet_write_def strict_ticks_of_Mndetprefix)

lemma strict_ticks_of_inj_on_ndet_write :
  ‹inj_on c A ⟹ ✓s(c!!a∈A → P a) = (⋃a∈{a ∈ A. P a ≠ ⊥}. ✓s(P a))›
  by (auto simp add: strict_ticks_of_ndet_write)

lemma strict_ticks_of_write : ‹✓s(c!a → P) = (if P = ⊥ then {} else ✓s(P))›
  unfolding write_def by (simp add: strict_ticks_of_Mprefix)



lemma strict_ticks_of_Ndet_subset : ‹✓s(P ⊓ Q) ⊆ ✓s(P) ∪ ✓s(Q)›
  unfolding strict_ticks_of_def by (auto simp add: Ndet_projs)

lemma strict_ticks_of_Det_subset : ‹✓s(P □ Q) ⊆ ✓s(P) ∪ ✓s(Q)›
  unfolding strict_ticks_of_def by (auto simp add: Det_projs)

lemma strict_ticks_of_Sliding_subset : ‹✓s(P ⊳ Q) ⊆ ✓s(P) ∪ ✓s(Q)›
  unfolding strict_ticks_of_def by (auto simp add: Sliding_projs)


lemma strict_ticks_of_Renaming_subset : ‹✓s(Renaming P f g) ⊆ g ` ✓s(P)›
proof (intro subsetI)
  fix s assume ‹s ∈ ✓s(Renaming P f g)›
  then obtain u where ‹u @ [✓(s)] ∈ 𝒯 (Renaming P f g)›
    ‹u ∉ 𝒟 (Renaming P f g)› by (meson strict_ticks_of_memD)
  then obtain t r where ‹s = g r› ‹u = map (map_eventptick f g) t› ‹t @ [✓(r)] ∈ 𝒯 P› ‹t ∉ 𝒟 P›
    by (auto simp add: Renaming_projs append_eq_map_conv tick_eq_map_eventptick_iff)
      (use append_T_imp_tickFree front_tickFree_Nil in blast,
        metis append_assoc butlast_snoc front_tickFree_iff_tickFree_butlast map_eventptick_tickFree
        nonTickFree_n_frontTickFree non_tickFree_tick tickFree_append_iff tickFree_imp_front_tickFree)
  thus ‹s ∈ g ` ✓s(P)› by (auto intro: strict_ticks_of_memI is_processT9)
qed


lemma strict_ticks_of_inj_on_Renaming :
  ‹✓s(Renaming P f g) = g ` ✓s(P)› if ‹inj_on f α(P)›
proof (rule subset_antisym)
  show ‹✓s(Renaming P f g) ⊆ g ` ✓s(P)› by (fact strict_ticks_of_Renaming_subset)
next
  show ‹g ` ✓s(P) ⊆ ✓s(Renaming P f g)›
  proof (rule subsetI, elim imageE strict_ticks_of_memE)
    fix s r t assume ‹s = g r› ‹t @ [✓(r)] ∈ 𝒯 P› ‹t ∉ 𝒟 P›
    from ‹s = g r› ‹t @ [✓(r)] ∈ 𝒯 P›
    have ‹map (map_eventptick f g) t @ [✓(s)] ∈ 𝒯 (Renaming P f g)›
      by (auto simp add: T_Renaming)
    moreover have ‹map (map_eventptick f g) t @ [✓(s)] ∉ 𝒟 (Renaming P f g)›
    proof (rule ccontr)
      assume ‹¬ map (map_eventptick f g) t @ [✓(s)] ∉ 𝒟 (Renaming P f g)›
      then obtain u1 u2 where * : ‹ftF u2› ‹tF u1› ‹u1 ∈ 𝒟 P›
        ‹map (map_eventptick f g) t @ [✓(s)] = map (map_eventptick f g) u1 @ u2›
        by (auto simp add: D_Renaming)
      from "*"(1, 2, 4) obtain u2' where ‹u2 = u2' @ [✓(s)]›
        by (metis last_appendR map_eventptick_tickFree nonTickFree_n_frontTickFree
            non_tickFree_tick snoc_eq_iff_butlast tickFree_append_iff)
      obtain t1 t2 where ** : ‹t = t1 @ t2› ‹map (map_eventptick f g) t1 = map (map_eventptick f g) u1›
        by (metis "*"(4) ‹u2 = u2' @ [✓(s)]› append.assoc append_eq_map_conv butlast_snoc)
      moreover from "*"(2) ‹t @ [✓(r)] ∈ 𝒯 P› calculation have ‹t1 ∈ {t ∈ 𝒯 P. tF t}›
        by simp (metis is_processT3_TR_append map_eventptick_tickFree)
      moreover have ‹u1 ∈ {t ∈ 𝒯 P. tF t}› by (simp add: "*"(2) "*"(3) D_T)
      ultimately have ‹t1 = u1›
        by (intro inj_on_map_map_eventptick_T_tickFree[THEN inj_onD, OF ‹inj_on f α(P)›])
      with "*"(2, 3) "**"(1) ‹t @ [✓(r)] ∈ 𝒯 P› ‹t ∉ 𝒟 P› show False
        using T_imp_front_tickFree front_tickFree_dw_closed
          front_tickFree_nonempty_append_imp is_processT7 by simp blast
    qed
    ultimately show ‹s ∈ ✓s(Renaming P f g)› by (simp add: strict_ticks_of_memI)
  qed
qed



lemma strict_ticks_of_Seq_subset : ‹✓s(P ; Q) ⊆ (if ✓s(P) = {} then {} else ✓s(Q))›
proof (rule subsetI, elim strict_ticks_of_memE)
  show ‹t @ [✓(r)] ∈ 𝒯 (P ; Q) ⟹ t ∉ 𝒟 (P ; Q) ⟹
        r ∈ (if ✓s(P) = {} then {} else ✓s(Q))› for r t
    by (simp add: Seq_projs strict_ticks_of_def)
      (metis (no_types, lifting) T_imp_front_tickFree T_nonTickFree_imp_decomp
        append_T_imp_tickFree butlast_append butlast_snoc is_processT7 is_processT9
        last_appendR last_snoc non_tickFree_tick tickFree_Nil tickFree_append_iff)
qed


lemma strict_ticks_of_Sync_subset : ‹✓s(P ⟦S⟧ Q) ⊆ ✓s(P) ∩ ✓s(Q)›
proof (rule subsetI)
  fix r assume ‹r ∈ ✓s(P ⟦S⟧ Q)›
  then obtain t where ‹t @ [✓(r)] ∈ 𝒯 (P ⟦S⟧ Q)› ‹t @ [✓(r)] ∉ 𝒟 (P ⟦S⟧ Q)› ‹t ∉ 𝒟 (P ⟦S⟧ Q)›
    by (meson strict_ticks_of_memE is_processT9)
  from this(1, 2) obtain t_P t_Q
    where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
      ‹(t @ [✓(r)]) setinterleaves ((t_P, t_Q), range tick ∪ ev ` S)›
    unfolding Sync_projs by blast
  then obtain t_P' t_Q'
    where * : ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(r)]› ‹t_P' ∈ 𝒯 P› ‹t_Q' ∈ 𝒯 Q›
      ‹t setinterleaves ((t_P', t_Q'), range tick ∪ ev ` S)›
    by (metis SyncWithTick_imp_NTF T_imp_front_tickFree is_processT3_TR_append)
  have ‹t_P' ∉ 𝒟 P›
  proof (rule ccontr)
    assume ‹¬ t_P' ∉ 𝒟 P›
    with "*"(4, 5) have ‹t ∈ 𝒟 (P ⟦S⟧ Q)›
      by (simp add: D_Sync) (use front_tickFree_Nil in blast)
    with ‹t ∉ 𝒟 (P ⟦S⟧ Q)› show False ..
  qed
  moreover have ‹t_Q' ∉ 𝒟 Q›
  proof (rule ccontr)
    assume ‹¬ t_Q' ∉ 𝒟 Q›
    with "*"(3, 5) have ‹t ∈ 𝒟 (P ⟦S⟧ Q)›
      by (simp add: D_Sync) (use front_tickFree_Nil setinterleaving_sym in blast)
    with ‹t ∉ 𝒟 (P ⟦S⟧ Q)› show False ..
  qed
  ultimately show ‹r ∈ ✓s(P) ∩ ✓s(Q)›
    using "*"(1, 2) ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› 
    by (meson IntI is_processT9 strict_ticks_of_memI)
qed


(*<*)
end
  (*>*)