Theory Deterministic_Processes

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 *
 * 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
 *
 * * 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.
 *
 * 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 HOLDER 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.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

chapter ‹An Excursion into Determinism›

(*<*)
theory Deterministic_Processes
  imports "HOL-CSP_PTick"
begin
  (*>*)

text ‹
This chapter is a preliminary work.
Indeed, later in the construction, we will define the notion of Procomata which comes
in different flavours, in particular deterministic ones.
We will establish then that such ProcOmata produce deterministic processes,
a classical notion in CSP that we formalize below.
›

text ‹
In a word, a deterministic process cannot refuse an event in which it can engage.
More formally, if term‹s @ [e] ∈ 𝒯 P›, then term‹(s, {e}) ∉ ℱ (P)›.
In this theory, we follow the proof sketch given in cite‹"roscoe:csp:1998"›
for characterizing deterministic processes as maximal elements for the
failure-divergence refinement term‹(⊑FD)›.
Other lemmas are proved with respect to CSP operators.
›


section ‹Accepts initials›

text ‹This notion is a weak version of determinism.
      It captures the idea of being deterministic for one step.›

subsection ‹Definition›

unbundle option_type_syntax

definition accepts_initials :: ‹('a, 'r) processptick ⇒ bool› (‹determ0›)
  where ‹determ0 P ≡ ∀e ∈ P0. {e} ∉ ℛ P›

lemma accepts_initialsI : ‹(⋀e. e ∈ P0 ⟹ {e} ∉ ℛ P) ⟹ determ0 P›
  and accepts_initialsD : ‹determ0 P ⟹ e ∈ P0 ⟹ {e} ∉ ℛ P›
  by (simp_all add: accepts_initials_def)


lemma accepts_initials_def_bis:
  ‹determ0 P ⟷ (∀e ∈ P0. ∀X ∈ ℛ P. e ∉ X)›
  by (auto simp add: accepts_initials_def)
    (metis Refusals_iff Un_upper1 insert_Diff insert_is_Un is_processT4)

lemma accepts_initialsI_bis : ‹(⋀e X. e ∈ P0 ⟹ X ∈ ℛ P ⟹ e ∉ X) ⟹ determ0 P›
  and accepts_initialsD_bis : ‹determ0 P ⟹ e ∈ P0 ⟹ X ∈ ℛ P ⟹ e ∉ X›
  by (simp_all add: accepts_initials_def_bis)



subsection ‹First properties›


lemma accepts_initials_STOP [simp] : ‹determ0 STOP›
  by (simp add: accepts_initials_def)

lemma accepts_initials_SKIP [simp] : ‹determ0 (SKIP r)›
  by (simp add: accepts_initials_def Refusals_iff F_SKIP)

lemma not_accepts_initials_BOT [simp] : ‹¬ determ0 ⊥›
  by (simp add: accepts_initials_def Refusals_iff F_BOT)


lemma accepts_initials_imp_initial_tick_iff_is_SKIP:
  ‹determ0 P ⟹ ✓(r) ∈ P0 ⟷ P = SKIP r›
proof (rule iffI)
  show ‹P = SKIP r ⟹ ✓(r) ∈ P0› by simp
next
  assume assms : ‹determ0 P› ‹✓(r) ∈ P0›
  hence initials_is : ‹P0 = {✓(r)}› 
    by (auto simp add: accepts_initials_def initials_def Refusals_iff subset_iff)
      (metis append_self_conv2 is_processT6_TR_notin singletonD)
  show ‹P = SKIP r›
  proof (subst SKIP_F_iff[symmetric], unfold failure_refine_def, safe)
    from assms show ‹(s, X) ∈ ℱ P ⟹ (s, X) ∈ ℱ (SKIP r)› for s X
      by (cases s, auto simp add: F_SKIP accepts_initials_def_bis Refusals_iff dest!: F_T)
        (metis initials_is initials_memI singletonD,
          metis T_imp_front_tickFree eventptick.disc(2) front_tickFree_Cons_iff
          initials_is initials_memI singletonD)
  qed
qed

lemma accepts_initials_imp_not_initial_tick_iff_is_STOP_or_some_initial_ev:
  ‹determ0 P ⟹ (range tick ∩ P0 = {}) ⟷ P = STOP ∨ (∃e. ev e ∈ P0)›
  by (simp add: disjoint_iff image_iff)
    (metis accepts_initials_imp_initial_tick_iff_is_SKIP all_not_in_conv eventptick.exhaust
      eventptick.simps(3) initials_SKIP initials_empty_iff_STOP singletonD)



subsection ‹Monotonicity›

lemma mono_accepts_initials_F: ‹P ⊑F Q ⟹ determ0 P ⟹ determ0 Q›
  by (frule anti_mono_initials_F)
    (auto simp add: failure_refine_def accepts_initials_def Refusals_iff subset_iff)

lemma mono_accepts_initials_FD: ‹P ⊑FD Q ⟹ determ0 P ⟹ determ0 Q›
  using leFD_imp_leF mono_accepts_initials_F by blast

lemma mono_accepts_initials: ‹P ⊑ Q ⟹ determ0 P ⟹ determ0 Q›
  by (drule le_approx_lemma_F, fold failure_refine_def) (rule mono_accepts_initials_F)


lemma restriction_adm_accepts_initials [restriction_adm_processptick_simpset, simp] :
  ‹adm↓ (λx. determ0 (f x))› if ‹cont↓ f›
for f :: ‹'b :: restriction ⇒ ('a, 'r) processptick›
proof (rule restriction_adm_subst)
  from ‹cont↓ f› show ‹cont↓ f› .
next
  show ‹adm↓ (determ0 :: ('a, 'r) processptick ⇒ bool)›
  proof (rule restriction_admI)
    fix σ and Σ :: ‹('a, 'r) processptick›
    assume ‹σ ─↓→ Σ› ‹determ0 (σ n)› for n
    show ‹determ0 Σ›
    proof (rule accepts_initialsI)
      fix e assume ‹e ∈ Σ0›
      from ‹σ ─↓→ Σ› obtain n0
        where * : ‹Σ ↓ Suc (Suc 0) = σ n0 ↓ Suc (Suc 0)›
        by (blast dest: restriction_tendstoD)
      with ‹e ∈ Σ0› have ‹e ∈ (σ n0)0›
        by (metis initials_restriction_processptick nat.distinct(1))
      with ‹determ0 (σ n0)› have ‹{e} ∉ ℛ (σ n0)›
        by (fact accepts_initialsD)
      with "*" show ‹{e} ∉ ℛ Σ›
        by (metis Refusals_iff F_restriction_processptick_Suc_length_iff_F
            list.size(3) restriction_related_pred)
    qed
  qed
qed



subsection ‹Behaviour on Operators›

lemma accepts_initials_Mprefix [simp] : ‹determ0 (□a ∈ A → P a)›
  by (simp add: accepts_initials_def initials_Mprefix Refusals_iff F_Mprefix)

lemma accepts_initials_write0 [simp] : ‹determ0 (a → P)›
  by (simp add: write0_def)

lemma accepts_initials_write [simp] : ‹determ0 (c!a → P)›
  by (simp add: write_def)

lemma accepts_initials_read [simp] : ‹determ0 (c?a∈A → P a)›
  by (simp add: read_def)


lemma accepts_initials_Ndet_iff:
  ‹determ0 (P ⊓ Q) ⟷ determ0 P ∧ determ0 Q ∧ P0 = Q0›
  by (auto simp add: accepts_initials_def initials_Ndet Refusals_iff F_Ndet)
    (metis CollectI F_T Un_iff append_Nil initials_def is_processT1 is_processT5_S7 singletonD)+

lemma accepts_initials_GlobalNdet_iff:
  ‹determ0 (⊓a ∈ A. P a) ⟷
   (∀a ∈ A. determ0 (P a) ∧ (∀b ∈ A. (P a)0 = (P b)0))›
  by (auto simp add: accepts_initials_def initials_GlobalNdet Refusals_iff F_GlobalNdet)
    (metis CollectI append_Nil initials_def is_processT1_TR is_processT5_S7 singletonD)+

lemma accepts_initials_Mndetprefix_iff:
  ‹determ0 (⊓a ∈ A → P a) ⟷ (∃a. A ⊆ {a})›
  by (simp add: Mndetprefix_GlobalNdet accepts_initials_GlobalNdet_iff initials_write0) blast

lemma accepts_initials_ndet_write_iff:
  ‹determ0 (c!!a ∈ A → P a) ⟷ (∃b. c ` A ⊆ {b})›
  by (simp add: ndet_write_def accepts_initials_Mndetprefix_iff)


lemma accepts_initials_SKIPS_iff :
  ‹determ0 (SKIPS R) ⟷ R = {} ∨ (∃r. R = {r})›
  by (simp add: SKIPS_def accepts_initials_GlobalNdet_iff) blast



lemma accepts_initials_Det : 
  ‹determ0 (P □ Q) ⟷ P = STOP ∨ Q = STOP ∨ range tick ∩ P0 ∩ Q0 ≠ {} ∨
                                              range tick ∩ (P0 ∪ Q0) = {}›
  (is ‹_ ⟷ ?rhs›) if accepts_initials : ‹determ0 P› ‹determ0 Q›
proof (cases ‹P = ⊥›; cases ‹Q = ⊥›)
  show ‹accepts_initials (P □ Q) ⟷ ?rhs› if non_BOT : ‹P ≠ ⊥› ‹Q ≠ ⊥›
  proof (rule iffI)
    show ‹?rhs ⟹ determ0 (P □ Q)›
    proof (elim disjE)
      show ‹P = STOP ⟹ determ0 (P □ Q)› ‹Q = STOP ⟹ determ0 (P □ Q)›
        by (simp_all add: accepts_initials)
    next
      from non_BOT accepts_initials
      show ‹range tick ∩ P0 ∩ Q0 ≠ {} ⟹ determ0 (P □ Q)›
        ‹range tick ∩ (P0 ∪ Q0) = {} ⟹ determ0 (P □ Q)›
        by (simp_all add: accepts_initials_def initials_def Refusals_iff
            Det_projs BOT_iff_Nil_D disjoint_iff)
          (metis append_Nil is_processT6_TR_notin singletonD)
    qed
  next
    have * : ‹⟦Q ≠ STOP; ✓(r) ∈ P0; ✓(r) ∉ Q0; determ0 P; determ0 (P □ Q)⟧ ⟹ False›
      for P Q :: ‹('a, 'r) processptick› and r
      by (metis Un_iff accepts_initials_imp_initial_tick_iff_is_SKIP ex_in_conv
          initials_Det initials_SKIP initials_empty_iff_STOP singletonD)
    show ‹determ0 (P □ Q) ⟹ ?rhs›
      by (simp add: disjoint_iff) (metis "*" Det_commute accepts_initials rangeE)
  qed
qed (use not_accepts_initials_BOT accepts_initials in auto)


lemma accepts_initials_GlobalDet :
  ‹determ0 (□a ∈ A. P a)› if ‹⋀a. a ∈ A ⟹ determ0 (P a)›
  ‹range tick ∩ (⋂a ∈ A. (P a)0) ≠ {} ∨ range tick ∩ (⋃a ∈ A. (P a)0) = {}›
proof (use that(2) in ‹elim disjE›)
  from that(1) show ‹range tick ∩ (⋂a∈A. (P a)0) ≠ {} ⟹ determ0 (□a ∈ A. P a)›
    by (auto simp add: accepts_initials_def initials_GlobalDet Refusals_iff F_GlobalDet)
      (meson is_processT8,
        metis accepts_initials_imp_initial_tick_iff_is_SKIP
        initials_SKIP initials_memI singleton_iff that(1))
next
  from that(1) show ‹range tick ∩ (⋃a∈A. (P a)0) = {} ⟹ determ0 (□a ∈ A. P a)›
    by (auto simp add: accepts_initials_def initials_GlobalDet Refusals_iff F_GlobalDet)
      (blast, metis BOT_iff_Nil_D not_accepts_initials_BOT that(1),
        metis UN_I disjoint_iff initials_memI rangeI)
qed


lemma accepts_initials_Seqptick :
  ‹determ0 (P ;✓ Q) ⟷ (∀r. ✓(r) ∈ P0 ⟶ determ0 (Q r))› if ‹determ0 P›
proof (intro iffI allI impI)
  show ‹determ0 (P ;✓ Q) ⟹ ✓(r) ∈ P0 ⟹ determ0 (Q r)› for r
    by (simp add: accepts_initials_imp_initial_tick_iff_is_SKIP ‹determ0 P›)
next
  have ‹P ≠ ⊥› using not_accepts_initials_BOT that by blast
  show ‹determ0 (P ;✓ Q)› if * : ‹∀r. ✓(r) ∈ P0 ⟶ determ0 (Q r)›
  proof (rule accepts_initialsI)
    fix e assume ‹e ∈ (P ;✓ Q)0›
    then consider a where ‹e = ev a› ‹ev a ∈ P0› | r where ‹✓(r) ∈ P0› ‹e ∈ (Q r)0›
      by (simp add: initials_Seqptick ‹P ≠ ⊥›) blast
    thus ‹{e} ∉ ℛ (P ;✓ Q)›
    proof cases
      from ‹determ0 P› ‹P ≠ ⊥› show ‹e = ev a ⟹ ev a ∈ P0 ⟹ {e} ∉ ℛ (P ;✓ Q)› for a
        unfolding accepts_initials_def_bis Refusals_def_bis
        by (simp add: Seqptick_projs BOT_iff_Nil_D ref_Seqptick_def)
          (metis ‹determ0 P› accepts_initials_imp_initial_tick_iff_is_SKIP eventptick.distinct(1)
                 initials_SKIP initials_memI insertI1 singletonD)
    next
      show ‹✓(r) ∈ P0 ⟹ e ∈ (Q r)0 ⟹ {e} ∉ ℛ (P ;✓ Q)› for r
        by (simp add: ‹determ0 P› accepts_initialsD accepts_initials_imp_initial_tick_iff_is_SKIP "*")
    qed
  qed
qed

corollary accepts_initials_Seq :
  ‹determ0 (P ; Q) ⟷ (P0 ∩ range tick = {} ∨ determ0 Q)› if ‹determ0 P›
  by (fold Seqptick_const, unfold accepts_initials_Seqptick[OF that]) fast


lemma (in Syncptick_locale) accepts_initials_Syncptick :
  ‹determ0 (P ⟦S⟧✓ Q)› if ‹determ0 P› ‹determ0 Q›
proof (rule accepts_initialsI)
  from ‹determ0 P› ‹determ0 Q› have ‹P ≠ ⊥› ‹Q ≠ ⊥› by auto
  fix e assume ‹e ∈ (P ⟦S⟧✓ Q)0›
  with ‹P ≠ ⊥› ‹Q ≠ ⊥› consider
    a where ‹e = ev a› ‹a ∈ S ∧ ev a ∈ P0 ∧ ev a ∈ Q0 ∨ a ∉ S ∧ (ev a ∈ P0 ∨ ev a ∈ Q0)›
  | r_s r s where ‹e = ✓(r_s)› ‹r ⊗✓ s = ⌊r_s⌋› ‹✓(r) ∈ P0› ‹✓(s) ∈ Q0›
    by (auto simp add: initials_Syncptick split: if_split_asm)
  thus ‹{e} ∉ ℛ (P ⟦S⟧✓ Q)›
  proof cases
    fix a assume ‹e = ev a› ‹a ∈ S ∧ ev a ∈ P0 ∧ ev a ∈ Q0 ∨ a ∉ S ∧ (ev a ∈ P0 ∨ ev a ∈ Q0)›
    from this(2) show ‹{e} ∉ ℛ (P ⟦S⟧✓ Q)›
    proof (elim disjE conjE)
      show ‹{e} ∉ ℛ (P ⟦S⟧✓ Q)› if ‹ev a ∈ P0› ‹ev a ∈ Q0›
      proof (rule notI)
        assume ‹{e} ∈ ℛ (P ⟦S⟧✓ Q)›
        with ‹P ≠ ⊥› ‹Q ≠ ⊥› obtain X_P X_Q
          where ‹([], X_P) ∈ ℱ P› ‹([], X_Q) ∈ ℱ Q› ‹e ∈ super_ref_Syncptick (⊗✓) X_P S X_Q›
          by (auto simp add: Refusals_iff F_Syncptick BOT_iff_Nil_D dest: Nil_setinterleavesptick)
        from this(3) have ‹ev a ∈ X_P ∨ ev a ∈ X_Q›
          by (auto simp add: ‹e = ev a› super_ref_Syncptick_def)
        with ‹ev a ∈ P0› ‹ev a ∈ Q0› ‹([], X_P) ∈ ℱ P› ‹([], X_Q) ∈ ℱ Q› show False
          by (fold Refusals_iff) (metis accepts_initialsD_bis ‹determ0 P› ‹determ0 Q›)
      qed
    next
      show ‹{e} ∉ ℛ (P ⟦S⟧✓ Q)› if ‹a ∉ S› ‹ev a ∈ P0›
      proof (rule notI)
        assume ‹{e} ∈ ℛ (P ⟦S⟧✓ Q)›
        with ‹P ≠ ⊥› ‹Q ≠ ⊥› obtain X_P X_Q
          where ‹([], X_P) ∈ ℱ P› ‹([], X_Q) ∈ ℱ Q› ‹e ∈ super_ref_Syncptick (⊗✓) X_P S X_Q›
          by (auto simp add: Refusals_iff F_Syncptick BOT_iff_Nil_D dest: Nil_setinterleavesptick)
        from this(3) have ‹ev a ∈ X_P›
          by (simp add: ‹e = ev a› ‹a ∉ S› super_ref_Syncptick_def)
        with ‹ev a ∈ P0› ‹([], X_P) ∈ ℱ P› show False
          by (fold Refusals_iff) (metis accepts_initialsD_bis ‹determ0 P›)
      qed
    next
      show ‹{e} ∉ ℛ (P ⟦S⟧✓ Q)› if ‹a ∉ S› ‹ev a ∈ Q0›
      proof (rule notI)
        assume ‹{e} ∈ ℛ (P ⟦S⟧✓ Q)›
        with ‹P ≠ ⊥› ‹Q ≠ ⊥› obtain X_P X_Q
          where ‹([], X_P) ∈ ℱ P› ‹([], X_Q) ∈ ℱ Q› ‹e ∈ super_ref_Syncptick (⊗✓) X_P S X_Q›
          by (auto simp add: Refusals_iff F_Syncptick BOT_iff_Nil_D dest: Nil_setinterleavesptick)
        from this(3) have ‹ev a ∈ X_Q›
          by (simp add: ‹e = ev a› ‹a ∉ S› super_ref_Syncptick_def)
        with ‹ev a ∈ Q0› ‹([], X_Q) ∈ ℱ Q› show False
          by (fold Refusals_iff) (metis accepts_initialsD_bis ‹determ0 Q›)
      qed
    qed
  next
    fix r_s r s assume ‹e = ✓(r_s)› ‹r ⊗✓ s = ⌊r_s⌋› ‹✓(r) ∈ P0› ‹✓(s) ∈ Q0›
    show ‹{e} ∉ ℛ (P ⟦S⟧✓ Q)›
    proof (rule notI)
      assume ‹{e} ∈ ℛ (P ⟦S⟧✓ Q)›
      with ‹P ≠ ⊥› ‹Q ≠ ⊥› obtain X_P X_Q
        where ‹([], X_P) ∈ ℱ P› ‹([], X_Q) ∈ ℱ Q› ‹e ∈ super_ref_Syncptick (⊗✓) X_P S X_Q›
        by (auto simp add: Refusals_iff F_Syncptick BOT_iff_Nil_D dest: Nil_setinterleavesptick)
      from this(3) have ‹✓(r) ∈ X_P›
        by (simp flip:  ‹r ⊗✓ s = ⌊r_s⌋› add: ‹e = ✓(r_s)› super_ref_Syncptick_def)
          (metis Refusals_iff ‹([], X_Q) ∈ ℱ Q› ‹✓(s) ∈ Q0› ‹r ⊗✓ s = ⌊r_s⌋›
            accepts_initials_def_bis inj_tick_join that(2))
      with ‹✓(r) ∈ P0› ‹([], X_P) ∈ ℱ P› show False
        by (fold Refusals_iff) (metis accepts_initialsD_bis ‹determ0 P›)
    qed
  qed
qed

corollary accepts_initials_Sync:
  ‹determ0 P ⟹ determ0 Q ⟹ determ0 (P ⟦S⟧ Q)›
  by (metis SyncClassic.accepts_initials_Syncptick SyncClassic_is_Sync)


lemma accepts_initials_Renaming : ‹determ0 (Renaming P f g)› if ‹determ0 P›
proof -
  from ‹determ0 P› have ‹P ≠ ⊥› by auto
  with ‹determ0 P› show ‹determ0 (Renaming P f g)›
    by (simp add: accepts_initials_def initials_Renaming Refusals_iff F_Renaming vimage_def BOT_iff_Nil_D)
      (metis (full_types) accepts_initials_def Refusals_iff accepts_initials_def_bis mem_Collect_eq)
qed


lemma accepts_initials_Throw_iff : ‹determ0 (P Θ a ∈ A. Q a) ⟷ determ0 P›
  using D_F by (auto simp add: accepts_initials_def initials_Throw Refusals_iff F_Throw)



lemma accepts_initials_Sliding:
  ‹determ0 P ⟹ determ0 Q ⟹ determ0 (P ⊳ Q) ⟷
   P = STOP ∨ P0 ⊆ Q0 ∧ (range tick ∩ P0 ≠ {} ∨ range tick ∩ Q0 = {})›
  by (auto simp add: Sliding_def accepts_initials_Ndet_iff accepts_initials_Det initials_Det)




(* lemma accepts_initials_Interrupt: ‹accepts_initials (P △ Q) ⟷ accepts_initials P ∧ (✓ ∉ P0 ∨ accepts_initials Q)›
  apply (cases ‹P = ⊥›, solves ‹auto simp add: Interrupt_BOT_absorb(2) not_accepts_initials_BOT›)
  apply (cases ‹Q = ⊥›, solves ‹auto simp add: Interrupt_BOT_absorb(1) not_accepts_initials_BOT›)
  apply (simp add: accepts_initials_def initials_Interrupt Refusals_iff F_Interrupt BOT_iff_D)
  apply safe
  oops *)


(* lemma accepts_initials_Hiding: ‹accepts_initials P ⟹ accepts_initials (P \ S)›
  oops
 *)




subsection ‹Characterizations with After›

context After
begin

text ‹Interesting results about the fact that we can express a process
      with const‹Mprefix› and const‹After››

lemma leFD_SKIPS_Det_Mprefix_After:
  ‹P ⊑FD SKIPS {r. ✓(r) ∈ P0} □ (□a ∈ {a. ev a ∈ P0} → P after a)› (is ‹P ⊑FD ?rhs›)
proof (unfold failure_divergence_refine_def failure_refine_def divergence_refine_def, safe)
  show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 P› for s
    by (auto simp add: D_Det D_SKIPS D_Mprefix D_After)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ P› for s X
  proof (cases s)
    show ‹s = [] ⟹ (s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ P›
      by (simp add: F_Det SKIPS_projs STOP_projs F_Mprefix  
          F_After disjoint_iff image_iff split: if_split_asm)
        (metis initials_memI append_Nil eventptick.exhaust is_processT1_TR is_processT5_S7,
          metis CollectD append.left_neutral initials_def is_processT6_TR_notin)
  next
    show ‹s = e # s' ⟹ (s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ P› for e s'
      by (auto simp add: F_Det SKIPS_projs STOP_projs F_Mprefix  
          F_After disjoint_iff image_iff split: if_split_asm)
        (metis CollectD append_butlast_last_id initials_def last_ConsL list.distinct(1) tick_T_F)
  qed
qed


lemma accepts_initials_imp_eq_Mprefix_After:
  ‹P = (  if ∃r. ✓(r) ∈ P0 then SKIP (THE r. ✓(r) ∈ P0)
        else □a ∈ {e. ev e ∈ P0} → P after a)› (is ‹P = ?rhs›)
  if ‹determ0 P›
proof -
  from not_accepts_initials_BOT ‹determ0 P› have non_BOT: ‹P ≠ ⊥› by blast
  note initial_tick_iff_is_SKIP = accepts_initials_imp_initial_tick_iff_is_SKIP[OF ‹determ0 P›]

  have * : ‹?rhs = (SKIPS {r. ✓(r) ∈ P0}) □
                   (□a ∈ {e. ev e ∈ P0} → P after a)› (is ‹?rhs = ?rhs_bis›)
    by (simp, rule impI, elim exE, simp add: initial_tick_iff_is_SKIP)

  show ‹P = ?rhs›
  proof (rule FD_antisym)
    show ‹P ⊑FD ?rhs› by (unfold "*") (fact leFD_SKIPS_Det_Mprefix_After)
  next
    show ‹?rhs ⊑FD P›
    proof (unfold failure_divergence_refine_def failure_refine_def divergence_refine_def, safe)
      from non_BOT show ‹s ∈ 𝒟 P ⟹ s ∈ 𝒟 ?rhs› for s
        by (cases s; simp add: D_Det D_SKIP D_STOP D_Mprefix BOT_iff_Nil_D
            image_iff D_After initial_tick_iff_is_SKIP)
          (metis BOT_iff_tick_D initials_memI D_T D_imp_front_tickFree eventptick.disc(2)
            eventptick.exhaust front_tickFree_Cons_iff initials_SKIP non_BOT singletonD)
    next
      have * : ‹∃r. ✓(r) ∈ P0 ⟹ ∃!r. ✓(r) ∈ P0›
        by (metis eventptick.inject(2) initial_tick_iff_is_SKIP initials_SKIP singletonD)
      show ‹(t, X) ∈ ℱ P ⟹ (t, X) ∈ ℱ ?rhs› for t X
      proof (cases t)
        from "*" show ‹t = [] ⟹ (t, X) ∈ ℱ P ⟹ (t, X) ∈ ℱ ?rhs›
          by (simp add: add: F_Mprefix disjoint_iff image_iff initial_tick_iff_is_SKIP)
            (metis (lifting) ‹determ0 P› Refusals_iff[of X P]
              accepts_initialsD_bis[of P _ X] the_equality[of ‹λr. P = SKIP r›])
      next
        from "*" show ‹t = e # t' ⟹ (t, X) ∈ ℱ P ⟹ (t, X) ∈ ℱ ?rhs› for e t'
          by (cases e, simp_all add: F_Mprefix F_After disjoint_iff image_iff initial_tick_iff_is_SKIP)
            (metis F_T eventptick.distinct(1) initials_SKIP initials_memI singletonD,
              metis (mono_tags, lifting) F_T initial_tick_iff_is_SKIP initials_memI the_equality)
      qed
    qed
  qed
qed



theorem is_some_Mprefix_iff:
  ‹(∃A Q. P = □a ∈ A → Q a) ⟷ range tick ∩ P0 = {} ∧ accepts_initials P›
  for P :: ‹('a, 'r) processptick›
proof (intro iffI exI)
  show ‹∃A Q. P = Mprefix A Q ⟹ range tick ∩ P0 = {} ∧ accepts_initials P›
    by (auto simp add: initials_Mprefix image_iff disjoint_iff)
next
  from accepts_initials_imp_eq_Mprefix_After
  show ‹range tick ∩ P0 = {} ∧ accepts_initials P ⟹
        P = □a ∈ {e. ev e ∈ P0} → P after a›
    by (meson disjoint_iff rangeI)
qed


lemma tick_not_initial_imp_STOP_Ndet_Mndetprefix_After_FD:
  ‹range tick ∩ P0 = {} ⟹ STOP ⊓ (□a ∈ {e. ev e ∈ P0} → P after a) ⊑FD P›
  by (cases ‹P = ⊥›, solves ‹simp›,
      auto simp add: refine_defs Ndet_projs F_STOP Mprefix_projs After_projs BOT_iff_Nil_D)
    (metis initials_memI F_T Int_iff empty_iff eventptick.exhaust neq_Nil_conv rangeI,
      metis initials_memI D_T disjoint_iff eventptick.exhaust neq_Nil_conv rangeI)

― ‹With this we could obtain something about const‹CHAOS› and const‹tickFree›
    and term‹𝒟 P = {}› but we already have this.›

lemma ‹lifelock_free P ⟷ 𝒟 P = {} ∧ (∀t ∈ 𝒯 P. tF t)›
  using lifelock_free_is_non_terminating non_terminating_is_right nonterminating_implies_div_free by blast



lemma STOP_Ndet_SKIPS_Ndet_Mprefix_After_leF :
  ‹STOP ⊓ SKIPS {r. ✓(r) ∈ P0} ⊓ (□a ∈ {e. ev e ∈ P0} → P after a) ⊑F P›
  (is ‹_ ⊓ ?lhs1 ⊓ ?lhs2 ⊑F P›)
proof (unfold failure_refine_def, safe)
  fix t X assume ‹(t, X) ∈ ℱ P›
  then consider ‹t = []› | r where ‹t = [✓(r)]› ‹r ∈ {r. ✓(r) ∈ P0}›
    | a t' where ‹t = ev a # t'› ‹a ∈ {a. ev a ∈ P0}›
    by (cases t, simp_all) (metis F_T F_imp_front_tickFree eventptick.exhaust
        front_tickFree_Cons_iff initials_memI is_ev_def)
  thus ‹(t, X) ∈ ℱ (STOP ⊓ ?lhs1 ⊓ ?lhs2)›
  proof cases
    show ‹t = [] ⟹ (t, X) ∈ ℱ (STOP ⊓ ?lhs1 ⊓ ?lhs2)› by (simp add: F_Ndet F_STOP)
  next
    fix r assume ‹t = [✓(r)]›
    with ‹(t, X) ∈ ℱ P› have ‹(t, X) ∈ ℱ (?lhs1)›
      by (auto simp add: F_SKIPS intro!: initials_memI' F_T)
    thus ‹(t, X) ∈ ℱ (STOP ⊓ ?lhs1 ⊓ ?lhs2)› by (simp add: F_Ndet)
  next
    fix a t' assume ‹t = ev a # t'›
    with ‹(t, X) ∈ ℱ P› have ‹(t, X) ∈ ℱ ?lhs2›
      by (auto simp add: F_Mprefix F_After intro!: initials_memI F_T)
    thus ‹(t, X) ∈ ℱ (STOP ⊓ ?lhs1 ⊓ ?lhs2)› by (simp add: F_Ndet)
  qed
qed

lemma non_BOT_imp_Mprefix_After_leD :
  ‹□a ∈ {e. ev e ∈ P0} → P after a ⊑D P› (is ‹_?lhs ⊑D P›) if ‹P ≠ ⊥›
proof (unfold divergence_refine_def, rule subsetI)
  fix t assume ‹t ∈ 𝒟 P›
  with ‹P ≠ ⊥› obtain a t' where ‹t = ev a # t'›
    by (cases t, simp add: BOT_iff_Nil_D, simp add: BOT_iff_tick_D)
      (metis D_imp_front_tickFree eventptick.exhaust front_tickFree_Cons_iff is_ev_def)
  with ‹t ∈ 𝒟 P› show ‹t ∈ 𝒟 ?lhs›
    by (auto simp add: D_Mprefix D_After intro: D_T initials_memI)
qed

lemma non_BOT_imp_STOP_Ndet_SKIPS_Ndet_Mprefix_After_leFD :
  ‹P ≠ ⊥ ⟹ STOP ⊓ SKIPS {r. ✓(r) ∈ P0} ⊓ (□a ∈ {e. ev e ∈ P0} → P after a) ⊑FD P›
  by (rule leF_leD_imp_leFD[OF STOP_Ndet_SKIPS_Ndet_Mprefix_After_leF])
    (use non_BOT_imp_Mprefix_After_leD Ndet_D_self_right trans_D in blast)




theorem singl_initial_imp_equals_prefix_After:
  ‹P = (if UNIV ∉ ℛ P then a → P after a else STOP ⊓ (a → P after a))›
  if initials_is : ‹initials P = {ev a}›
proof (split if_split, intro conjI impI)
  assume not_all_refusals : ‹UNIV ∉ ℛ P›
  have $ : ‹e ≠ ev a ⟹ [e] ∉ 𝒯 P› for e using initials_is unfolding initials_def by auto
  { assume ‹{ev a} ∈ ℛ P›
    from is_processT5[rule_format, of ‹[]› ‹{ev a}› P ‹UNIV - {ev a}›, folded Refusals_iff,
        simplified this T_F_spec, simplified, rule_format, OF "$", simplified]
    have ‹UNIV ∈ ℛ P› .
    with not_all_refusals have False by simp
  } hence not_in_refusal: ‹{ev a} ∉ ℛ P› by blast
  show ‹P = a → P after a›
    by (unfold write0_def, subst accepts_initials_imp_eq_Mprefix_After)
      (solves ‹simp add: accepts_initials_def initials_is not_in_refusal›,
        auto simp add: that(1) intro: mono_Mprefix_eq)
next
  assume all_refusals : ‹¬ UNIV ∉ ℛ P›
  from tick_not_initial_imp_STOP_Ndet_Mndetprefix_After_FD[of P]
  have *  : ‹STOP ⊓ (a → P after a) ⊑FD P›
    by (simp add: that(1) Mprefix_singl image_iff)
  from leFD_SKIPS_Det_Mprefix_After[of P] all_refusals
  have ** : ‹P ⊑FD STOP ⊓ (a → P after a)›
    by (auto simp add: refine_defs that(1) write0_projs Mprefix_projs
        Ndet_projs STOP_projs Refusals_iff)
      (meson is_processT4 subset_UNIV)
  from "**" "*" show ‹P = STOP ⊓ (a → P after a)› by (fact FD_antisym)
qed


lemma ‹{ev e} ∉ ℛ P ⟹ ev e ∈ P0›
  by (simp add: Refusals_iff initials_def) 
    (metis is_processT1_TR is_processT5_S7 self_append_conv2 singletonD)

end



section ‹Deterministic process›

subsection ‹Definition›

definition deterministic :: ‹('a, 'r) processptick ⇒ bool› (‹determ›)
  where ‹determ P ≡ ∀ s e. s @ [e] ∈ 𝒯 P ⟶ (s, {e}) ∉ ℱ (P)›

lemma deterministicI : ‹(⋀t e. t @ [e] ∈ 𝒯 P ⟹ (t, {e}) ∉ ℱ (P)) ⟹ determ P›
  and deterministicD : ‹determ P ⟹ t @ [e] ∈ 𝒯 P ⟹ (t, {e}) ∉ ℱ (P)›
  by (simp_all add: deterministic_def)

lemma deterministic_STOP [simp] : ‹determ STOP›
  and deterministic_SKIP [simp] : ‹determ (SKIP r)›
  by (simp_all add: deterministic_def T_STOP SKIP_projs)

lemma deterministic_div_free : ‹determ P ⟹ 𝒟 P = {}›
  by (auto simp add: deterministic_def)
    (metis D_T D_imp_front_tickFree append_butlast_last_id div_butlast_when_non_tickFree_iff
      front_tickFree_single is_processT7 is_processT8 tickFree_Nil)

lemma not_deterministic_BOT [simp] : ‹¬ determ ⊥›
  using BOT_iff_Nil_D deterministic_div_free by blast


subsection ‹Monotonicity›

lemma mono_deterministic_F: ‹P ⊑F Q ⟹ determ P ⟹ determ Q›
  by (meson T_F_spec deterministic_def failure_refine_def subset_iff)

lemma mono_deterministic_FD: ‹P ⊑FD Q ⟹ determ P ⟹ determ Q›
  using leFD_imp_leF mono_deterministic_F by blast

lemma mono_deterministic: ‹P ⊑ Q ⟹ determ P ⟹ determ Q›
  using le_approx_imp_le_ref mono_deterministic_FD by auto


lemma restriction_adm_deterministic [restriction_adm_processptick_simpset, simp] :
  ‹adm↓ (λx. determ (f x))› if ‹cont↓ f›
for f :: ‹'b :: restriction ⇒ ('a, 'r) processptick›
proof (rule restriction_adm_subst)
  from ‹cont↓ f› show ‹cont↓ f› .
next
  show ‹adm↓ (determ :: ('a, 'r) processptick ⇒ bool)›
  proof (rule restriction_admI)
    fix σ and Σ :: ‹('a, 'r) processptick›
    assume ‹σ ─↓→ Σ› ‹determ (σ n)› for n
    show ‹determ Σ›
    proof (rule deterministicI)
      fix t e assume ‹t @ [e] ∈ 𝒯 Σ›
      from ‹σ ─↓→ Σ› obtain n0
        where * : ‹Σ ↓ Suc (length (t @ [e])) = σ n0 ↓ Suc (length (t @ [e]))›
        by (blast dest: restriction_tendstoD)
      with ‹t @ [e] ∈ 𝒯 Σ› have ‹t @ [e] ∈ 𝒯 (σ n0)›
        by (metis T_restriction_processptick_Suc_length_iff_T)
      with ‹deterministic (σ n0)› have ‹(t, {e}) ∉ ℱ (σ n0)›
        by (fact deterministicD)
      with "*" show ‹(t, {e}) ∉ ℱ Σ›
        by (metis F_restriction_processptick_Suc_length_iff_F
            length_append_singleton restriction_related_pred)
    qed
  qed
qed



subsection ‹Characterization as Maximal›

subsubsection ‹Some preliminary work›

definition is_processT :: ‹('a, 'r) traceptick set ⇒ bool›
  where ‹is_processT T ≡
         [] ∈ T ∧ (∀t ∈ T. ftF t) ∧ (∀t u. t @ u ∈ T ⟶ t ∈ T) ∧
         (∀t r e. t @ [✓(r)] ∈ T ⟶ e ≠ ✓(r) ⟶ t @ [e] ∉ T)›

typedef ('a, 'r) processT = ‹{T :: ('a, 'r) traceptick set . is_processT T}›
proof (rule exI)
  show ‹{[]} ∈ {T. is_processT T}› unfolding is_processT_def by simp
qed

setup_lifting type_definition_processT


lift_definition TracesT ::
  ‹('a, 'r) processT ⇒ ('a, 'r) traceptick set› (‹𝒯T›)
  is ‹λP. Rep_processT P› .

lemma ProcessT_eq_spec : ‹T = U ⟷ 𝒯T T = 𝒯T U›
  by (simp add: Rep_processT_inject TracesT.rep_eq)

lemma is_processT_1 : ‹[] ∈ 𝒯T P›
  and is_processT_2 : ‹s ∈ 𝒯T P ⟹ ftF s›
  and is_processT_3 : ‹s @ t ∈ 𝒯T P ⟹ s ∈ 𝒯T P›
  and is_processT_4 : ‹s @ [✓(r)] ∈ 𝒯T P ⟹ e ≠ ✓(r) ⟹ s @ [e] ∉ 𝒯T P›
  by (transfer, meson Rep_processT[simplified, unfolded is_processT_def])+


lemmas is_processT_def_bis = is_processT_def[of ‹Rep_processT _›, folded TracesT.rep_eq]



lift_definition processptick_of_processT ::
  ‹('a, 'r) processT ⇒ ('a, 'r) processptick›
  is ‹λT. ({(s, X). s ∈ 𝒯T T ∧ X ⊆ - {e. s @ [e] ∈ 𝒯T T}}, {})›
  by (auto simp add: is_process_def FAILURES_def DIVERGENCES_def
      intro: is_processT_1 is_processT_2 is_processT_3)
    (meson is_processT_4)



lemma F_processptick_of_processT :
  ‹ℱ (processptick_of_processT T) = {(s, X). s ∈ 𝒯T T ∧ X ⊆ - {e. s @ [e] ∈ 𝒯T T}}›
  and D_processptick_of_processT :
  ‹𝒟 (processptick_of_processT T) = {}›
  and T_processptick_of_processT :
  ‹𝒯 (processptick_of_processT T) = 𝒯T T›
  by (simp_all add: Failures_def FAILURES_def Divergences_def DIVERGENCES_def
      Traces_def TRACES_def processptick_of_processT.rep_eq) blast

lemmas processptick_of_processT_projs = F_processptick_of_processT
  D_processptick_of_processT T_processptick_of_processT


subsubsection ‹Now the big results›

lemma bij_betw_det :
  ‹bij_betw processptick_of_processT UNIV {P :: ('a, 'r) processptick. determ P}›
  (is ‹bij_betw processptick_of_processT ?S1 ?S2›)
proof (intro bij_betw_imageI)
  show ‹inj_on processptick_of_processT ?S1›
    by (rule inj_onI) (auto simp add: Process_eq_spec processptick_of_processT_projs ProcessT_eq_spec)
next
  show ‹processptick_of_processT ` ?S1 = ?S2›
  proof (intro subset_antisym subsetI; clarify)
    show ‹determ (processptick_of_processT P)› for P :: ‹('a, 'r) processT›
      by (rule deterministicI) (simp add: processptick_of_processT_projs)
  next
    fix P :: ‹('a, 'r) processptick›
    assume det : ‹deterministic P›
    hence * : ‹Rep_processT (Abs_processT (𝒯 P)) = 𝒯 P›
      by (intro Abs_processT_inverse)
        (simp add: deterministic_def is_processT_def is_processT2_TR,
          metis T_F_spec is_processT3 is_processT6_notin singletonD)
    show ‹P ∈ processptick_of_processT ` ?S1›
    proof (subst image_iff, rule bexI)
      show ‹P = processptick_of_processT (Abs_processT (𝒯 P))›
        by (auto intro!: Process_eq_optimizedI simp add: processptick_of_processT_projs
            TracesT_def "*" det deterministic_div_free subset_iff F_T)
          (meson det deterministic_def empty_subsetI insert_subset is_processT,
            use is_processT5_S7 in blast) 
    next
      show ‹Abs_processT (𝒯 P) ∈ ?S1› by (simp add: TracesT_def "*")
    qed
  qed
qed



lemma SKIPS_is_GlobalDet_SKIP : ‹SKIPS R = □r ∈ R. SKIP r›
  by (auto simp add: Process_eq_spec SKIPS_projs GlobalDet_projs SKIP_projs)

lemma SKIP_Ndet_SKIP_is_SKIP_Det_SKIP : ‹SKIP r ⊓ SKIP s = SKIP r □ SKIP s›
  by (auto simp add: Process_eq_spec Det_projs Ndet_projs SKIP_projs)


theorem P_FD_some_det :
  ― ‹In the generalization, since several terminations may occur after
      the same trace in the initial process, we have to specify a choice.›
  fixes termination_choice :: ‹('a, 'r) traceptick ⇒ 'r›
  assumes ‹⋀t. ∃r. t @ [✓(r)] ∈ 𝒯 P ⟹ termination_choice t ∈ {r. t @ [✓(r)] ∈ 𝒯 P}›
  defines ‹T ≡ {t ∈ 𝒯 P. ∀t' < t. (∃r. t' @ [✓(r)] ∈ 𝒯 P) ⟶ t = t' @ [✓(termination_choice t')]}›
  shows ‹P ⊑FD processptick_of_processT (Abs_processT T)›
proof (unfold failure_divergence_refine_def failure_refine_def divergence_refine_def, intro conjI)
  show ‹𝒟 (processptick_of_processT (Abs_processT T)) ⊆ 𝒟 P› by (simp add: D_processptick_of_processT)
next
  have * : ‹T ∈ {T. is_processT T}›
    by (auto simp add: T_def is_processT_def T_imp_front_tickFree intro: is_processT3_TR_append)
      (metis prefix_prefix append_eq_first_pref_spec less_list_def nless_le self_append_conv,
        metis less_self)

  show ‹ℱ (processptick_of_processT (Abs_processT T)) ⊆ ℱ P›
  proof safe
    fix s X assume ‹(s, X) ∈ ℱ (processptick_of_processT (Abs_processT T))›
    hence ‹s ∈ 𝒯 P›
      by (simp add: F_processptick_of_processT TracesT_def Abs_processT_inverse[OF "*"]) (simp add: T_def)
    show ‹(s, X) ∈ ℱ P›
    proof (cases ‹∃r. s @ [✓(r)] ∈ 𝒯 P›)
      assume ‹∃r. s @ [✓(r)] ∈ 𝒯 P›
      hence ‹s @ [✓(termination_choice s)] ∈ 𝒯 P› by (metis assms(1) mem_Collect_eq)
      with ‹(s, X) ∈ ℱ (processptick_of_processT (Abs_processT T))› have ‹✓(termination_choice s) ∉ X›
        unfolding F_processptick_of_processT TracesT.abs_eq Abs_processT_inverse[OF "*"]
        by (simp add: subset_iff T_def)
          (metis prefix_snoc append_T_imp_tickFree nless_le
            non_tickFree_tick not_Cons_self2 tickFree_append_iff)
      with ‹s @ [✓(termination_choice s)] ∈ 𝒯 P› show ‹(s, X) ∈ ℱ P›
        by (metis  is_processT6_TR_notin)
    next
      assume ‹∄r. s @ [✓(r)] ∈ 𝒯 P›
      with ‹(s, X) ∈ ℱ (processptick_of_processT (Abs_processT T))› have ‹X ⊆ - {e. s @ [e] ∈ 𝒯 P}›
        unfolding F_processptick_of_processT TracesT.abs_eq Abs_processT_inverse[OF "*"]
        by (simp add: subset_iff T_def)
          (metis prefix_snoc append_T_imp_tickFree nless_le
            non_tickFree_tick not_Cons_self2 tickFree_append_iff)
      with is_processT5_S7[OF ‹s ∈ 𝒯 P›] show ‹(s, X) ∈ ℱ P› by blast
    qed
  qed
qed



theorem deterministic_iff_maximal_for_leFD:
  ‹determ P ⟷ (∀Q. P ⊑FD Q ⟶ P = Q)› for P :: ‹('a, 'r) processptick›
  ― ‹see TPC, chapter 9)›
proof (intro iffI allI impI)
  fix Q assume ‹determ P› and ‹P ⊑FD Q›
  from ‹P ⊑FD Q› have no_div : ‹𝒟 P = {}› ‹𝒟 Q = {}› and F_subset : ‹ℱ Q ⊆ ℱ P›
    by (simp_all add: ‹determ P› deterministic_div_free refine_defs)

  have same_T : ‹𝒯 P = 𝒯 Q›
  proof (rule subset_antisym)
    show ‹𝒯 P ⊆ 𝒯 Q›
    proof (rule ccontr)
      assume ‹¬ 𝒯 P ⊆ 𝒯 Q›
      then obtain s e where * : ‹s @ [e] ∈ min_elems (𝒯 P - 𝒯 Q)›
        by (metis DiffD2 Diff_eq_empty_iff Nil_elem_T elem_min_elems min_elems4 rev_exhaust)
      hence ‹s ∈ 𝒯 Q› unfolding min_elems_def 
        by simp (metis DiffI T_F_spec is_processT3 less_self)
      with "*" have ‹(s, {e}) ∈ ℱ Q› 
        by (metis Diff_iff elem_min_elems is_processT5_S7 singletonD)
      from set_mp[OF F_subset this] have ‹(s, {e}) ∈ ℱ P› .
      moreover have ‹(s, {e}) ∉ ℱ P› by (metis "*" Diff_iff ‹determ P› deterministicD elem_min_elems)
      ultimately show False by blast
    qed
  next
    show ‹𝒯 Q ⊆ 𝒯 P› by (simp add: F_subset F_subset_imp_T_subset)
  qed

  have same_F : ‹ℱ P = ℱ Q›
  proof (rule subset_antisym)
    show ‹ℱ P ⊆ ℱ Q›
    proof (rule ccontr)
      assume ‹¬ ℱ P ⊆ ℱ Q›
      then obtain s X where * : ‹(s, X) ∈ ℱ P - ℱ Q› ‹X ≠ {}› 
        by (metis DiffI T_F_spec same_T subrelI)

      have ‹e ∈ X ⟹ s @ [e] ∉ 𝒯 P› for e
        by (metis "*"(1) DiffD1 ‹determ P› deterministicD insert_Diff insert_is_Un is_processT4 sup_ge1)
      thus False by (metis "*"(1) DiffE F_T is_processT5_S7 same_T)
    qed
  next
    show ‹ℱ Q ⊆ ℱ P› by (fact F_subset)
  qed
  show ‹P = Q› by (simp add: Process_eq_spec failure_refine_def divergence_refine_def no_div same_F)

next
  define termination_choice where ‹termination_choice s ≡ (SOME r. s @ [✓(r)] ∈ 𝒯 P)› for s
  have $ : ‹∃r. s @ [✓(r)] ∈ 𝒯 P ⟹ termination_choice s ∈ {r. s @ [✓(r)] ∈ 𝒯 P}› for s
    by (simp add: termination_choice_def) (meson someI)

  define T where ‹T ≡ {s ∈ 𝒯 P. ∀s' < s. (∃r. s' @ [✓(r)] ∈ 𝒯 P) ⟶ s = s' @ [✓(termination_choice s')]}›
  have * : ‹T ∈ {T. is_processT T}›
    by (auto simp add: T_def is_processT_def T_imp_front_tickFree intro: is_processT3_TR_append)
      (metis prefix_prefix append_eq_first_pref_spec less_list_def nless_le self_append_conv,
        metis less_self)
  assume maximal : ‹∀Q. P ⊑FD Q ⟶ P = Q›
  with "$" P_FD_some_det T_def have ‹P = processptick_of_processT (Abs_processT T)› by blast
  moreover have ‹Abs_processT T ∈ {P. ∀s r e. s @ [✓(r)] ∈ 𝒯T P ⟶ e ≠ ✓(r) ⟶ s @ [e] ∉ 𝒯T P}›
    by (simp add: TracesT_def Abs_processT_inverse[OF "*"])
      (metis "*" is_processT_def mem_Collect_eq)
  ultimately show ‹determ P› using bij_betwE[OF bij_betw_det] by blast
qed


lemma ‹determ P ⟹ X ∈ ℛ P ⟹ X ⊆ - P0›
  unfolding deterministic_def Refusals_iff initials_def
  by auto (metis insert_Diff insert_is_Un process_charn self_append_conv2 sup_ge1)




text ‹We have the immediate powerful corollaries.›

corollary (in After) deterministic_process_eq_SKIPS_Det_Mprefix_After :
  ‹determ P ⟹ P = SKIPS {r. ✓(r) ∈ P0} □ (□a ∈ {a. ev a ∈ P0} → P after a)›
  by (simp add: deterministic_iff_maximal_for_leFD leFD_SKIPS_Det_Mprefix_After)


lemma deterministic_imp_initial_tick_iff_eq_SKIP [simp] :
  ‹determ P ⟹ ✓(r) ∈ P0 ⟷ P = SKIP r›
  by (meson deterministic_iff_maximal_for_leFD dual_order.refl initial_tick_iff_FD_SKIP)


lemma deterministic_imp_constraints_on_initials :
  ‹determ P ⟹ P0 = {} ∨ {a. ev a ∈ P0} = {} ∧ (∃r. P0 = {✓(r)}) ∨
                {a. ev a ∈ P0} ≠ {} ∧ {r. ✓(r) ∈ P0} = {}›
  by auto (metis deterministic_imp_initial_tick_iff_eq_SKIP eventptick.exhaust initials_SKIP)


corollary (in After) deterministic_process_eq_SKIP_or_Mprefix_After :
  ‹determ P ⟹ P = (if ∃r. ✓(r) ∈ P0 then SKIP (THE r. P0 = {✓(r)})
                     else □a ∈ {a. ev a ∈ P0} → P after a)›
  by (subst deterministic_process_eq_SKIPS_Det_Mprefix_After)
    (auto simp add: inj_on_eq_iff[OF inj_SKIP])



subsection ‹Characterization with After›

lemma (in AfterExt) deterministic_iff_accepts_initials_Aftertrace:
  ‹determ P ⟷ (∀t ∈ 𝒯 P. tF t ⟶ determ0 (P after𝒯 t))›
proof (intro iffI ballI impI)
  show ‹determ P ⟹ t ∈ 𝒯 P ⟹ tF t ⟹ determ0 (P after𝒯 t)› for t
    by (rule accepts_initialsI)
      (simp add: initials_def Refusals_iff T_Aftertrace_eq F_Aftertrace_eq deterministic_def)
next
  show ‹determ P› if ‹∀t∈𝒯 P. tF t ⟶ determ0 (P after𝒯 t)›
  proof (rule deterministicI)
    fix t e assume ‹t @ [e] ∈ 𝒯 P›
    have ‹t ∈ 𝒯 P› and ‹tF t›
      by (meson prefixI ‹t @ [e] ∈ 𝒯 P› is_processT3_TR)
        (use ‹t @ [e] ∈ 𝒯 P› append_T_imp_tickFree in blast)
    with ‹t ∈ 𝒯 P› that[rule_format, OF this] show ‹t @ [e] ∈ 𝒯 P ⟹ (t, {e}) ∉ ℱ P›
      by (simp add: accepts_initials_def Refusals_iff initials_def T_Aftertrace_eq F_Aftertrace_eq)
  qed
qed



subsection ‹Operators preserving Determinism›

lemma deterministic_Mprefix_iff :
  ‹determ (□a ∈ A → P a) ⟷ (∀a ∈ A. determ (P a))›
  by (auto simp add: deterministic_def Mprefix_projs) (metis append_Cons)

corollary deterministic_write0_iff : ‹determ (a → P) ⟷ determ P›
  unfolding write0_def by (simp add: deterministic_Mprefix_iff)

corollary deterministic_write_iff  : ‹determ (c!a → P) ⟷ determ P›
  unfolding write_def by (simp add: deterministic_Mprefix_iff)

corollary deterministic_inj_on_read_iff :
  ‹inj_on c A ⟹ determ (c?a ∈ A → P a) ⟷ (∀a ∈ A. determ (P a))›
  unfolding read_def by (simp add: deterministic_Mprefix_iff)



lemma deterministic_inj_Renaming :
  ‹determ (Renaming P f g)› if ‹inj f› ‹inj g› ‹determ P›
proof (rule deterministicI)
  have $ : ‹inj (map_eventptick f g)› by (simp add: eventptick.inj_map that(1,2))
  fix t e
  assume ‹t @ [e] ∈ 𝒯 (Renaming P f g)›
  then obtain t1 where * : ‹t1 ∈ 𝒯 P› ‹t @ [e] = map (map_eventptick f g) t1›
    by (simp add: T_Renaming deterministic_div_free[OF ‹determ P›]) blast
  have ‹(s1, map_eventptick f g -` {e}) ∈ ℱ P ⟹ t ≠ map (map_eventptick f g) s1› for s1 
  proof (rule ccontr, clarify)
    assume assms : ‹(s1, map_eventptick f g -` {e}) ∈ ℱ P› ‹t = map (map_eventptick f g) s1› 
    from assms(2) "*"(2) have ‹t1 = s1 @ [inv (map_eventptick f g) e]›
      by (cases t1 rule: rev_cases; simp)
        (metis (mono_tags, opaque_lifting) "$" inj_map_eq_map inv_f_f)
    from deterministicD[OF ‹deterministic P› "*"(1)[unfolded this]]
    have ‹(s1, {inv (map_eventptick f g) e}) ∉ ℱ P› .
    also have ‹{inv (map_eventptick f g) e} = map_eventptick f g -` {e}›
      using inj_vimage_singleton[OF "$", of e] "*"(2)
        ‹t1 = s1 @ [inv (map_eventptick f g) e]› by (auto simp add: "$")
    finally have ‹(s1, map_eventptick f g -` {e}) ∉ ℱ P› .
    with assms(1) show False by simp
  qed
  thus ‹(t, {e}) ∉ ℱ (Renaming P f g)›
    by (auto simp add: F_Renaming deterministic_div_free[OF ‹determ P›])
qed

lemma deterministic_bij_Renaming_iff :
  ‹determ (Renaming P f g) ⟷ determ P› if ‹bij f› and ‹bij g›
proof (rule iffI)
  show ‹determ (Renaming P f g) ⟹ determ P›
    by (metis Renaming_inv bij_betw_def deterministic_iff_maximal_for_leFD
        mono_Renaming_FD ‹bij f› ‹bij g›)
next
  show ‹determ P ⟹ determ (Renaming P f g)›
    by (simp add: bij_is_inj deterministic_inj_Renaming ‹bij f› ‹bij g›)
qed



lemma deterministic_Throw : ‹determ (P Θ a ∈ A. Q a)›
  if ‹determ P› ‹⋀a. a ∈ A ⟹ a ∈ α(P) ⟹ determ (Q a)›
proof (subst Throw_is_restrictable_on_events_of)
  show ‹determ (Throw P (A ∩ α(P)) Q)›
  proof (rule deterministicI)
    fix t e assume ‹t @ [e] ∈ 𝒯 (P Θ a ∈ (A ∩ α(P)). Q a)›
    moreover from ‹determ P› have ‹𝒟 P = {}›
      by (simp add: deterministic_div_free)
    ultimately consider
      (traceL) ‹t @ [e] ∈ 𝒯 P› ‹e ∉ ev ` (A ∩ α(P))› ‹set t ∩ ev ` (A ∩ α(P)) = {}›
      | (traceR) t1 a t2 where ‹t @ [e] = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` (A ∩ α(P)) = {}› ‹a ∈ A› ‹a ∈ α(P)› ‹t2 ∈ 𝒯 (Q a)›
      unfolding T_Throw by auto
    thus ‹(t, {e}) ∉ ℱ (P Θ a ∈ (A ∩ α(P)). Q a)›
    proof cases
      case traceL
      from traceL(1) ‹determ P› have ‹(t, {e}) ∉ ℱ P›
        by (simp add: deterministicD)
      with traceL(3) show ‹(t, {e}) ∉ ℱ (P Θ a ∈ (A ∩ α(P)). Q a)›
        by (auto simp add: F_Throw ‹𝒟 P = {}›)
    next
      case traceR
      from traceR(1) consider ‹t2 = []› ‹t = t1› ‹e = ev a›
        | t2' where ‹t2 = t2' @ [e]› ‹t = t1 @ ev a # t2'›
        by (cases t2 rule: rev_cases) simp_all
      thus ‹(t, {e}) ∉ ℱ (P Θ a ∈ (A ∩ α(P)). Q a)›
      proof cases
        assume ‹t2 = []› ‹t = t1› ‹e = ev a›
        from ‹determ P› traceR(2) have ‹(t1, {ev a}) ∉ ℱ P›
          by (simp add: deterministicD)
        with traceR(3) show ‹(t, {e}) ∉ ℱ (P Θ a ∈ (A ∩ α(P)). Q a)›
          by (auto simp add: ‹t = t1› ‹e = ev a› ‹𝒟 P = {}› F_Throw)
      next
        fix t2' assume ‹t2 = t2' @ [e]› ‹t = t1 @ ev a # t2'›
        from traceR(4, 5) have ‹determ (Q a)›
          by (rule ‹⋀a. a ∈ A ⟹ a ∈ α(P) ⟹ determ (Q a)›)
        with ‹t2 = t2' @ [e]› have ‹(t2', {e}) ∉ ℱ (Q a)›
          using traceR(6) by (simp add: deterministicD)
        with traceR(3-5) show ‹(t, {e}) ∉ ℱ (P Θ a ∈ (A ∩ α(P)). Q a)›
          by (simp add: ‹t = t1 @ ev a # t2'› ‹𝒟 P = {}› F_Throw Throw_T_third_clause_breaker)
      qed
    qed
  qed
qed



lemma T_snoc_tick_imp_no_continuation_if_deterministic : 
  ‹u = [] ∧ e = ✓(r)› if ‹determ P› ‹t @ u @ [e] ∈ 𝒯 P› ‹t @ [✓(r)] ∈ 𝒯 P›
proof -
  have * : ‹t @ [e] ∈ 𝒯 P ⟹ e = ✓(r)› for e
    by (metis deterministicD is_processT6_TR_notin singletonD that(1, 3))
  show ‹u = [] ∧ e = ✓(r)›
  proof (cases u)
    from "*" that(2) show ‹u = [] ⟹ u = [] ∧ e = ✓(r)› by auto
  next
    fix e' u'
    assume ‹u = e' # u'›
    with that(2) have ‹t @ [e'] ∈ 𝒯 P›
      by simp (metis F_T T_F append.assoc append_Cons append_Nil is_processT3)
    hence False
      by (metis "*" T_imp_front_tickFree ‹u = e' # u'› eventptick.disc(2) front_tickFree_append_iff
          not_Cons_self snoc_eq_iff_butlast that(2) tickFree_Cons_iff)
    thus ‹u = [] ∧ e = ✓(r)› by simp
  qed
qed

lemma T_snoc_ev_imp_no_tick_continuation_if_deterministic : 
  ‹u ≠ [] ∧ is_ev (hd u) ∨ is_ev e› if ‹determ P› ‹t @ u @ [e] ∈ 𝒯 P› ‹t @ [ev a] ∈ 𝒯 P›
proof -
  have ‹t @ [e] ∈ 𝒯 P ⟹ is_ev e› for e
    by (metis T_snoc_tick_imp_no_continuation_if_deterministic append.left_neutral
        eventptick.discI(1) eventptick.exhaust that(1,3))
  thus ‹u ≠ [] ∧ is_ev (hd u) ∨ is_ev e›
    by (metis T_imp_front_tickFree append_eq_appendI front_tickFree_append_iff
        list.exhaust_sel not_Cons_self snoc_eq_iff_butlast that(2) tickFree_Cons_iff)
qed



lemma deterministic_Seqptick : ‹determ (P ;✓ Q)›
  if ‹determ P› ‹⋀r. r ∈ ✓s(P) ⟹ determ (Q r)›
proof (rule deterministicI)
  fix t e assume ‹t @ [e] ∈ 𝒯 (P ;✓ Q)›
  moreover from ‹determ P› have ‹𝒟 P = {}›
    by (simp add: deterministic_div_free)
  ultimately consider a u where ‹e = ev a› ‹t = map (ev ∘ of_ev) u› ‹u @ [ev a] ∈ 𝒯 P› ‹tF u›
    | u v r where ‹t @ [e] = map (ev ∘ of_ev) u @ v› ‹u @ [✓(r)] ∈ 𝒯 P› ‹tF u› ‹v ∈ 𝒯 (Q r)› ‹v ≠ []›
    by (auto simp add: Seqptick_projs append_eq_map_conv append_eq_append_conv2 Cons_eq_append_conv)
      (metis Nil_is_append_conv append.right_neutral append_Nil not_Cons_self, blast,
        metis Cons_eq_appendI append_eq_appendI eq_Nil_appendI eventptick.collapse(1) is_processT3_TR_append)
  thus ‹(t, {e}) ∉ ℱ (P ;✓ Q)›
  proof cases
    show ‹e = ev a ⟹ t = map (ev ∘ of_ev) u ⟹ u @ [ev a] ∈ 𝒯 P ⟹ tF u ⟹ (t, {e}) ∉ ℱ (P ;✓ Q)› for a u
      by (auto simp add: tickFree_map_ev_of_ev_inj ‹𝒟 P = {}› Seqptick_projs ref_Seqptick_def map_eq_append_conv)
        (meson deterministicD empty_subsetI insertI1 insert_subset is_processT4 ‹determ P›,
          meson T_snoc_tick_imp_no_continuation_if_deterministic eventptick.distinct(1) ‹determ P›)
  next
    fix u v r assume ‹t @ [e] = map (ev ∘ of_ev) u @ v› ‹u @ [✓(r)] ∈ 𝒯 P› ‹tF u› ‹v ∈ 𝒯 (Q r)› ‹v ≠ []›
    from this(1, 5) obtain v' where ‹v = v' @ [e]› ‹t = map (ev ∘ of_ev) u @ v'›
      by (cases v rule: rev_cases) simp_all
    from ‹u @ [✓(r)] ∈ 𝒯 P› T_snoc_tick_imp_no_continuation_if_deterministic[OF ‹determ P›]
    have * : ‹map (ev ∘ of_ev) u @ v' = map (ev ∘ of_ev) w @ x ∧ w @ [✓(s)] ∈ 𝒯 P ⟹ w = u ∧ s = r› for w x s
      by (auto simp add: append_eq_append_conv2 map_eq_append_conv append_eq_map_conv append_T_imp_tickFree
                  dest!: tickFree_map_ev_of_ev_inj[THEN iffD1, rotated 2]) blast+
    have ‹determ (Q r)›
      by (metis ‹𝒟 P = {}› ‹u @ [✓(r)] ∈ 𝒯 P› empty_iff strict_ticks_of_memI that(2))
    with ‹v = v' @ [e]› ‹v ∈ 𝒯 (Q r)›
    have ‹(v', {e}) ∉ ℱ (Q r)› by (simp add: deterministicD)
    { fix v'' assume ‹(u @ v'', ref_Seqptick {e}) ∈ ℱ P› ‹tF v''› ‹v' = map (ev ∘ of_ev) v''›
      have ‹v'' = []›
        by (metis F_T F_imp_front_tickFree T_snoc_tick_imp_no_continuation_if_deterministic ‹(u @ v'', ref_Seqptick {e}) ∈ ℱ P›
            ‹tF v''› ‹u @ [✓(r)] ∈ 𝒯 P› front_tickFree_charn front_tickFree_nonempty_append_imp non_tickFree_tick ‹determ P›)
      with ‹(u @ v'', ref_Seqptick {e}) ∈ ℱ P› have ‹(u, {✓(r)}) ∈ ℱ P›
        by (simp add: ref_Seqptick_def)
          (meson UNIV_I UnCI empty_subsetI insert_subset is_processT4 rev_image_eqI)
      hence False by (simp add: ‹u @ [✓(r)] ∈ 𝒯 P› deterministicD ‹determ P›)
    }
    with "*" ‹(v', {e}) ∉ ℱ (Q r)› show ‹(t, {e}) ∉ ℱ (P ;✓ Q)›
      by (auto simp add: Seqptick_projs ‹𝒟 P = {}› ‹t = map (ev ∘ of_ev) u @ v'› append_eq_map_conv ‹tF u›
                        dest!: tickFree_map_ev_of_ev_inj[THEN iffD1, rotated 2])+
  qed
qed


corollary deterministic_Seq : ‹determ P ⟹ determ Q ⟹ determ (P ; Q)›
  by (metis Seqptick_const deterministic_Seqptick)




lemma (in After) initial_imp_deterministic_After:
  ‹ev e ∈ P0 ⟹ determ P ⟹ determ (P after e)›
  unfolding deterministic_def by (simp add: After_projs)

lemma (in AfterExt) initial_imp_deterministic_Aftertick:
  ‹e ∈ P0 ⟹ (case e of ✓(r) ⇒ determ (Ω P r)) ⟹
   determ P ⟹ determ (P after✓ e)›
  unfolding deterministic_def by (cases e) (simp_all add: T_Aftertick F_Aftertick)



subsection ‹Operators not (always) preserving Determinism›


lemma deterministic_imp_accepts_initials : ‹determ P ⟹ determ0 P›
  by (simp add: Refusals_iff accepts_initials_def deterministic_def initials_def)

corollary deterministic_SKIPS_iff : ‹determ (SKIPS R) ⟷ R = {} ∨ (∃r. R = {r})›
  by (metis SKIPS_empty SKIPS_singl_is_SKIP accepts_initials_SKIPS_iff
      deterministic_SKIP deterministic_STOP deterministic_imp_accepts_initials)




lemma deterministic_Det: 
  ‹determ P ⟹ determ Q ⟹
   range tick ∩ P0 ∩ Q0 ≠ {} ∨ P0 ∩ Q0 = {} ∧ range tick ∩ (P0 ∪ Q0) = {} ⟹ determ (P □ Q)›
proof (elim disjE conjE)
  show ‹determ P ⟹ determ Q ⟹ range tick ∩ P0 ∩ Q0 ≠ {} ⟹ determ (P □ Q)›
    by (auto simp add: deterministic_def Det_projs SKIP_projs)
next
  show ‹⟦determ P; determ Q; P0 ∩ Q0 = {}; range tick ∩ (P0 ∪ Q0) = {}⟧ ⟹ determ (P □ Q)›
    by (auto simp add: deterministic_def Det_projs disjoint_iff deterministic_div_free initials_def)
      (metis F_T append_Cons append_Nil is_processT3_TR_append neq_Nil_conv)+
qed




section ‹Application to Operational Semantics›


lemma (in OpSemFD) tickFree_trace_trans_preserves_deterministic:
  ‹(P :: ('a, 'r) processptick) FD↝* t Q ⟹ tF t ⟹ deterministic P ⟹ deterministic Q›
proof (induct rule: trace_trans.induct)
  show ‹P FD↝τ P' ⟹ deterministic P ⟹ deterministic P'› for P P' :: ‹('a, 'r) processptick›
    using deterministic_iff_maximal_for_leFD by blast
next
  show ‹tF [✓(r)] ⟹ deterministic P›
    for r :: ‹'r› and P :: ‹('a, 'r) processptick› by simp
next
  fix a P P' and t :: ‹('a, 'r) traceptick› and P'' :: ‹('a, 'r) processptick›
  assume ‹P FD↝⇘a⇙ P'› ‹tF (ev a # t)› ‹deterministic P›
    ‹tF t ⟹ deterministic P' ⟹ deterministic P''›
  from ‹P FD↝⇘a⇙ P'› ‹deterministic P› have ‹deterministic P'›
    using deterministic_iff_maximal_for_leFD ev_trans_is initial_imp_deterministic_After by blast
  with ‹tF t ⟹ deterministic P' ⟹ deterministic P''› ‹tickFree (ev a # t)›
  show ‹deterministic P''› by simp
qed

lemma deterministic_imp_Refusals_iff: ‹deterministic P ⟹ X ∈ ℛ P ⟷ X ∩ P0 = {}›
  by (auto simp add: Refusals_iff initials_def deterministic_def disjoint_iff)
    (metis append_Nil empty_subsetI insert_subset process_charn,
      metis Nil_elem_T append_Nil is_processT5_S7)


lemma (in OpSemFD) deterministic_F_trace_trans_reality_check:
  ‹deterministic P ⟹ tF t ⟹
   (t, X) ∈ ℱ (P :: ('a, 'r) processptick) ⟷ (∃Q. (P FD↝*t Q) ∧ X ∩ Q0 = {})›
  by (simp add: F_trace_trans_reality_check)
    (metis deterministic_imp_Refusals_iff tickFree_trace_trans_preserves_deterministic)



lemma ‹¬ deterministic ((a → SKIP undefined) □ SKIP undefined)›
  by (metis Det_commute FD_iff_eq_Ndet Sliding_SKIP Sliding_def Un_insert_right initials_write0 insertI1
      singletonD deterministic_iff_maximal_for_leFD eventptick.simps(4) initials_Det initials_SKIP)


(*<*)
end
  (*>*)