Theory After_Ext_Operator

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff.
 *
 * This file       : Extension of the After operator with a locale
 *
 * 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 ‹Extension of the After Operator›

section‹ The After‹✓› Operator ›

(*<*)
theory  After_Ext_Operator
  imports After_Operator 
begin
  (*>*)

locale AfterExt = After Ψ
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick ›
    ―‹Just declaring the types typ‹'a› and typ‹'r›.› +
  fixes Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
begin


subsection ‹Definition›

text ‹We just defined term‹P after e› for @{term [show_types] ‹P :: ('a, 'r) processptick›} 
      and @{term [show_types] ‹e :: 'a›}; in other words we cannot handle term‹✓(r)›.
      We now introduce a generalisation for @{term [show_types] ‹e :: ('a, 'r) eventptick›}.›

text ‹In the previous version, we agreed to get const‹STOP› after a termination,
      but only if term‹P› was not term‹⊥› since otherwise we kept term‹⊥›.
      We were not really sure about this choice, and we even introduced a variation
      where the result after a termination was always const‹STOP›. 
      In this new version we use a placeholder instead: term‹Ω›.
      We define term‹P› after term‹✓(r)› being equal to term‹Ω P r›.›

text ‹For the moment we have no additional assumption on term‹Ω›. This will be discussed later.›


definition Aftertick :: ‹[('a, 'r) processptick, ('a, 'r) eventptick] ⇒ ('a, 'r) processptick› (infixl ‹after✓› 86)
  where ‹P after✓ e ≡ case e of ev x ⇒ P after x | ✓(r) ⇒ Ω P r›


lemma not_initial_Aftertick:
  ‹e ∉ initials P ⟹ P after✓ e = (case e of ev x ⇒ Ψ P x | ✓(r) ⇒ Ω P r)›
  by (auto simp add: Aftertick_def After_BOT intro: not_initial_After split: eventptick.split)

lemma initials_Aftertick: 
  ‹(P after✓ e)0 =
   (case e of ✓(r) ⇒ (Ω P r)0
            | ev a ⇒ if ev a ∈ P0 then {e. [ev a, e] ∈ 𝒯 P} else (Ψ P a)0)›
  by (simp add: Aftertick_def initials_After split: eventptick.split) 


subsection ‹Projections›

lemma F_Aftertick: 
  ‹ℱ (P after✓ e) =
   (case e of ✓(r) ⇒ ℱ (Ω P r)
            | ev a ⇒ if ev a ∈ P0 then {(s, X). (ev a # s, X) ∈ ℱ P} else ℱ (Ψ P a))›
  by (simp add: Aftertick_def F_After split: eventptick.split)

lemma D_Aftertick:
  ‹𝒟 (P after✓ e) =
   (case e of ✓(r) ⇒ 𝒟 (Ω P r)
            | ev a ⇒ if ev a ∈ P0 then {s. ev a # s ∈ 𝒟 P} else 𝒟 (Ψ P a))›
  by (simp add: Aftertick_def D_After split: eventptick.split)

lemma T_Aftertick:
  ‹𝒯 (P after✓ e) =
   (case e of ✓(r) ⇒ 𝒯 (Ω P r)
            | ev a ⇒ if ev a ∈ P0 then {s. ev a # s ∈ 𝒯 P} else 𝒯 (Ψ P a))›
  by (simp add: Aftertick_def T_After split: eventptick.split)



subsection ‹Monotony›

lemma mono_Aftertick_T  :
  ‹e ∈ Q0 ⟹ (case e of ✓(r) ⇒ Ω P r ⊑T Ω Q r)  ⟹ P ⊑T Q  ⟹ P after✓ e ⊑T Q after✓ e›
  and mono_Aftertick_F  :
  ‹e ∈ Q0 ⟹ (case e of ✓(r) ⇒ Ω P r ⊑F Ω Q r)  ⟹ P ⊑F Q  ⟹ P after✓ e ⊑F Q after✓ e›
  and mono_Aftertick_D  :
  ‹e ∈ Q0 ⟹ (case e of ✓(r) ⇒ Ω P r ⊑D Ω Q r)  ⟹ P ⊑D Q  ⟹ P after✓ e ⊑D Q after✓ e›
  and mono_Aftertick_FD :
  ‹e ∈ Q0 ⟹ (case e of ✓(r) ⇒ Ω P r ⊑FD Ω Q r) ⟹ P ⊑FD Q ⟹ P after✓ e ⊑FD Q after✓ e›
  and mono_Aftertick_DT :
  ‹e ∈ Q0 ⟹ (case e of ✓(r) ⇒ Ω P r ⊑DT Ω Q r) ⟹ P ⊑DT Q ⟹ P after✓ e ⊑DT Q after✓ e›
  using mono_After_T mono_After_F mono_After_D mono_After_FD mono_After_DT
  by (auto simp add: Aftertick_def split: eventptick.split)

lemma mono_Aftertick :
  ‹⟦P ⊑ Q;
    (case e of ev a ⇒ (ev a ∈ Q0 ∨ Ψ P a ⊑ Ψ Q a));
    (case e of ✓(r) ⇒ Ω P r ⊑ Ω Q r)⟧ ⟹
   P after✓ e ⊑ Q after✓ e›
  by (force simp add: Aftertick_def split: eventptick.split intro: mono_After)



subsection ‹Behaviour of @{const [source] Aftertick} with const‹STOP›, const‹SKIP› and term‹⊥››

lemma Aftertick_STOP: ‹STOP after✓ e = (case e of ev a ⇒ Ψ STOP a | ✓(r) ⇒ Ω STOP r)›
  and Aftertick_SKIP: ‹SKIP r after✓ e = (case e of ev a ⇒ Ψ (SKIP r) a | ✓(s) ⇒ Ω (SKIP r) s)›
  and Aftertick_BOT : ‹⊥ after✓ e = (case e of ev x ⇒ ⊥ | ✓(r) ⇒ Ω ⊥ r)›
  by (simp_all add: Aftertick_def After_STOP After_SKIP After_BOT split: eventptick.split)


lemma Aftertick_is_BOT_iff:
  ‹P after✓ e = ⊥ ⟷ 
   (case e of ✓(r) ⇒ Ω P r = ⊥
            | ev a ⇒ if ev a ∈ P0 then [ev a] ∈ 𝒟 P else Ψ P a = ⊥)›
  by (simp add: Aftertick_def After_is_BOT_iff split: eventptick.split)



subsection ‹Behaviour of @{const [source] Aftertick} with Operators of session‹HOL-CSP››

text ‹Here again, we lose determinism.›

lemma Aftertick_Mprefix_is_Aftertick_Mndetprefix: 
  ‹a ∈ A ⟹ (□a ∈ A → P a) after✓ ev a = (⊓a ∈ A → P a) after✓ ev a›
  by (simp add: Aftertick_def After_Mprefix_is_After_Mndetprefix)

lemma Aftertick_Det_is_Aftertick_Ndet:
  ‹ev a ∈ P0 ∪ Q0 ⟹ (P □ Q) after✓ ev a = (P ⊓ Q) after✓ ev a›
  by (simp add: Aftertick_def After_Det_is_After_Ndet)

lemma Aftertick_Sliding_is_Aftertick_Ndet:
  ‹ev a ∈ P0 ∪ Q0 ⟹ (P ⊳ Q) after✓ ev a = (P ⊓ Q) after✓ ev a›
  by (simp add: Aftertick_def After_Sliding_is_After_Ndet)


lemma Aftertick_Ndet: 
  ‹(P ⊓ Q) after✓ e =
   (case e of ✓(r) ⇒ Ω (P ⊓ Q) r
            | ev a ⇒   if ev a ∈ P0 ∩ Q0
                      then P after✓ ev a ⊓ Q after✓ ev a
                      else   if ev a ∈ P0
                           then P after✓ ev a
                           else  if ev a ∈ Q0
                                then Q after✓ ev a
                                else Ψ (P ⊓ Q) a)›
  by (simp add: Aftertick_def After_Ndet split: eventptick.split)

lemma Aftertick_Det: 
  ‹(P □ Q) after✓ e =
   (case e of ✓(r) ⇒ Ω (P □ Q) r
            | ev a ⇒   if ev a ∈ P0 ∩ Q0
                      then P after✓ ev a ⊓ Q after✓ ev a
                      else   if ev a ∈ P0
                           then P after✓ ev a
                           else  if ev a ∈ Q0
                                then Q after✓ ev a
                                else Ψ (P □ Q) a)›
  by (simp add: Aftertick_def After_Det split: eventptick.split)

lemma Aftertick_Sliding: 
  ‹(P ⊳ Q) after✓ e =
   (case e of ✓(r) ⇒ Ω (P ⊳ Q) r
            | ev a ⇒   if ev a ∈ P0 ∩ Q0
                      then P after✓ ev a ⊓ Q after✓ ev a
                      else   if ev a ∈ P0
                           then P after✓ ev a
                           else  if ev a ∈ Q0
                                then Q after✓ ev a
                                else Ψ (P ⊳ Q) a)›
  by (simp add: Aftertick_def After_Sliding split: eventptick.split)


lemma Aftertick_Mprefix: 
  ‹(□ a ∈ A → P a) after✓ e =
   (case e of ✓(r) ⇒ Ω (□ a ∈ A → P a) r
            | ev a ⇒ if a ∈ A then P a else Ψ (□ a ∈ A → P a) a)›
  by (simp add: Aftertick_def After_Mprefix split: eventptick.split)

lemma Aftertick_Mndetprefix: 
  ‹(⊓ a ∈ A → P a) after✓ e =
   (case e of ✓(r) ⇒ Ω (⊓ a ∈ A → P a) r
            | ev a ⇒ if a ∈ A then P a else Ψ (⊓ a ∈ A → P a) a)›
  by (simp add: Aftertick_def After_Mndetprefix split: eventptick.split)

corollary Aftertick_write0:
  ‹(a → P) after✓ e =
   (case e of ✓(r) ⇒ Ω (a → P) r
            | ev b ⇒ if b = a then P else Ψ (a → P) b)›
  by (simp add: Aftertick_def After_write0 split: eventptick.split)

corollary ‹(a → P) after✓ ev a = P› by (simp add: Aftertick_write0)

corollary Aftertick_read:
  ‹(c?a∈A → P a) after✓ e =
   (case e of ✓(r) ⇒ Ω (c?a∈A → P a) r
            | ev b ⇒ if b ∈ c ` A then P (inv_into A c b) else Ψ (c?a∈A → P a) b)›
  by (simp add: Aftertick_def After_read split: eventptick.split)

corollary Aftertick_ndet_write:
  ‹(c!!a∈A → P a) after✓ e =
   (case e of ✓(r) ⇒ Ω (c!!a∈A → P a) r
            | ev b ⇒ if b ∈ c ` A then P (inv_into A c b) else Ψ (c!!a∈A → P a) b)›
  by (simp add: Aftertick_def After_ndet_write split: eventptick.split)


lemma Aftertick_Seq: 
  ‹(P ; Q) after✓ e =
   (case e of ✓(r) ⇒ Ω (P ; Q) r
            | ev a ⇒   if range tick ∩ P0 = {} ∨ (∀r. ✓(r) ∈ P0 ⟶ ev a ∉ Q0)
                      then if ev a ∈ P0 then P after✓ ev a ; Q else Ψ (P ; Q) a
                      else   if ev a ∈ P0 then (P after✓ ev a ; Q) ⊓ Q after✓ ev a
                           else Q after✓ ev a)›
  by (simp add: Aftertick_def After_Seq split: eventptick.split)


lemma Aftertick_Sync: 
  ‹(P ⟦S⟧ Q) after✓ e = 
   (case e of ✓(r) ⇒ Ω (P ⟦S⟧ Q) r
            | ev a ⇒   if P = ⊥ ∨ Q = ⊥ then ⊥
                      else   if ev a ∈ P0 ∩ Q0
                           then   if a ∈ S then P after✓ ev a ⟦S⟧ Q after✓ ev a
                                else (P after✓ ev a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after✓ ev a)
                           else   if ev a ∈ P0 ∧ a ∉ S then P after✓ ev a ⟦S⟧ Q
                                else   if ev a ∈ Q0 ∧ a ∉ S then P ⟦S⟧ Q after✓ ev a
                                     else Ψ (P ⟦S⟧ Q) a)›
  by (simp add: Aftertick_def After_Sync split: eventptick.split) 


lemma Hiding_FD_Hiding_Aftertick_if_initial_inside:
  ‹ev a ∈ P0 ⟹ a ∈ A ⟹ P \ A ⊑FD P after✓ ev a \ A›
  and Aftertick_Hiding_FD_Hiding_Aftertick_if_initial_notin:
  ‹ev a ∈ P0 ⟹ a ∉ A ⟹ (P \ A) after✓ ev a ⊑FD P after✓ ev a \ A›
  by (simp add: Aftertick_def Hiding_FD_Hiding_After_if_initial_inside)
    (simp add: Aftertick_def After_Hiding_FD_Hiding_After_if_initial_notin)


lemmas Hiding_F_Hiding_Aftertick_if_initial_inside = 
  Hiding_FD_Hiding_Aftertick_if_initial_inside[THEN leFD_imp_leF]
  and Aftertick_Hiding_F_Hiding_Aftertick_if_initial_notin = 
  Aftertick_Hiding_FD_Hiding_Aftertick_if_initial_notin[THEN leFD_imp_leF]
  and Hiding_D_Hiding_Aftertick_if_initial_inside = 
  Hiding_FD_Hiding_Aftertick_if_initial_inside[THEN leFD_imp_leD]
  and Aftertick_Hiding_D_Hiding_Aftertick_if_initial_notin = 
  Aftertick_Hiding_FD_Hiding_Aftertick_if_initial_notin[THEN leFD_imp_leD]
  and Hiding_T_Hiding_Aftertick_if_initial_inside = 
  Hiding_FD_Hiding_Aftertick_if_initial_inside[THEN leFD_imp_leF, THEN leF_imp_leT]   
  and Aftertick_Hiding_T_Hiding_Aftertick_if_initial_notin = 
  Aftertick_Hiding_FD_Hiding_Aftertick_if_initial_notin[THEN leFD_imp_leF, THEN leF_imp_leT]

corollary Hiding_DT_Hiding_Aftertick_if_initial_inside:
  ‹ev a ∈ P0 ⟹ a ∈ A ⟹ P \ A ⊑DT P after✓ ev a \ A›
  and Aftertick_Hiding_DT_Hiding_Aftertick_if_initial_notin: 
  ‹ev a ∈ P0 ⟹ a ∉ A ⟹ (P \ A) after✓ ev a ⊑DT P after✓ ev a \ A›
  by (simp add: Hiding_D_Hiding_Aftertick_if_initial_inside 
      Hiding_T_Hiding_Aftertick_if_initial_inside leD_leT_imp_leDT)
    (simp add: Aftertick_Hiding_D_Hiding_Aftertick_if_initial_notin 
      Aftertick_Hiding_T_Hiding_Aftertick_if_initial_notin leD_leT_imp_leDT)

end

text ‹As with locale‹After›, we need to "duplicate" the locale
      to formalize the result for the const‹Renaming› operator.›

locale AfterExtDuplicated = Aftertickα: AfterExt Ψα Ωα + Aftertickβ: AfterExt Ψβ Ωβ
  for Ψα :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ωα :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and Ψβ :: ‹[('b, 's) processptick, 'b] ⇒ ('b, 's) processptick›
    and Ωβ :: ‹[('b, 's) processptick, 's] ⇒ ('b, 's) processptick› 

sublocale AfterExtDuplicated ⊆ AfterDuplicated .
    ―‹Recovering @{thm [source] AfterDuplicated.After_Renaming}›

context AfterExtDuplicated
begin 

notation Aftertickα.After (infixl ‹afterα› 86)
notation Aftertickβ.After (infixl ‹afterβ› 86)
notation Aftertickα.Aftertick (infixl ‹after✓α› 86)
notation Aftertickβ.Aftertick (infixl ‹after✓β› 86)

lemma Aftertick_Renaming:
  ‹Renaming P f g after✓β e =
   (case e of ✓(s) ⇒ Ωβ (Renaming P f g) s
            | ev b ⇒   if P = ⊥ then ⊥
                      else   if ∃a. ev a ∈ P0 ∧ f a = b
                           then ⊓ a∈{a. ev a ∈ P0 ∧ f a = b}. Renaming (P afterα a) f g
                           else Ψβ (Renaming P f g) b)›
  by (auto simp add: Aftertickα.Aftertick_def Aftertickβ.Aftertick_def 
      After_Renaming split: eventptick.split)

end


context AfterExt ―‹Back to locale‹AfterExt›.›
begin

subsection ‹Behaviour of @{const [source] Aftertick} with Operators of session‹HOL-CSPM››

lemma Aftertick_GlobalDet_is_Aftertick_GlobalNdet:
  ‹ev a ∈ (⋃a ∈ A. (P a)0) ⟹
   (□ a ∈ A. P a) after✓ ev a = (⊓ a ∈ A. P a) after✓ ev a›
  by (simp add: Aftertick_def After_GlobalDet_is_After_GlobalNdet)

lemma Aftertick_GlobalNdet: 
  ‹(⊓ a ∈ A. P a) after✓ e =
   (case e of ✓(r) ⇒ Ω (⊓ a ∈ A. P a) r
            | ev a ⇒   if ev a ∈ (⋃a ∈ A. (P a)0)
                      then ⊓ x ∈ {x ∈ A. ev a ∈ (P x)0}. P x after✓ ev a
                      else Ψ (⊓ a ∈ A. P a) a)›
  and Aftertick_GlobalDet: 
  ‹(□ a ∈ A. P a) after✓ e = 
   (case e of ✓(r) ⇒ Ω (□ a ∈ A. P a) r
            | ev a ⇒   if ev a ∈ (⋃a ∈ A. (P a)0)
                      then ⊓ x ∈ {x ∈ A. ev a ∈ (P x)0}. P x after✓ ev a
                      else Ψ (□ a ∈ A. P a) a)›
  by (simp_all add: Aftertick_def After_GlobalNdet After_GlobalDet split: eventptick.split)


(* TODO: formulate and prove for MultiSync and MultiSeq *)


lemma Aftertick_Throw:
  ‹(P Θ a ∈ A. Q a) after✓ e = 
   (case e of ✓(r) ⇒ Ω (P Θ a ∈ A. Q a) r
            | ev a ⇒   if P = ⊥ then ⊥
                      else   if ev a ∈ P0
                           then   if a ∈ A
                                then Q a
                                else P after✓ ev a Θ a ∈ A. Q a
                           else Ψ (P Θ a ∈ A. Q a) a)›
  by (simp add: Aftertick_def After_Throw split: eventptick.split)


lemma Aftertick_Interrupt:
  ‹(P △ Q) after✓ e = 
   (case e of ✓(r) ⇒ Ω (P △ Q) r
            | ev a ⇒   if ev a ∈ P0 ∩ Q0
                      then Q after✓ ev a ⊓ (P after✓ ev a △ Q)
                      else   if ev a ∈ P0 ∧ ev a ∉ Q0
                           then P after✓ ev a △ Q
                           else   if ev a ∉ P0 ∧ ev a ∈ Q0
                                then Q after✓ ev a 
                                else Ψ (P △ Q) a)›
  by (simp add: Aftertick_def After_Interrupt split: eventptick.split)



subsection ‹Behaviour of @{const [source] Aftertick} with Reference Processes›

lemma Aftertick_DF: 
  ‹DF A after✓ e =
   (case e of ✓(r) ⇒ Ω (DF A) r
            | ev a ⇒ if a ∈ A then DF A else Ψ (DF A) a)›
  by (simp add: Aftertick_def After_DF split: eventptick.split)

lemma Aftertick_DFSKIPS:
  ‹DFSKIPS A R after✓ e =
   (case e of ✓(r) ⇒ Ω (DFSKIPS A R) r
            | ev a ⇒ if a ∈ A then DFSKIPS A R else Ψ (DFSKIPS A R) a)›
  by (simp add: Aftertick_def After_DFSKIPS split: eventptick.split)

lemma Aftertick_RUN:
  ‹RUN A after✓ e =
   (case e of ✓(r) ⇒ Ω (RUN A) r
            | ev a ⇒ if a ∈ A then RUN A else Ψ (RUN A) a)›
  by (simp add: Aftertick_def After_RUN split: eventptick.split)

lemma Aftertick_CHAOS:
  ‹CHAOS A after✓ e =
   (case e of ✓(r) ⇒ Ω (CHAOS A) r
            | ev a ⇒ if a ∈ A then CHAOS A else Ψ (CHAOS A) a)›
  by (simp add: Aftertick_def After_CHAOS split: eventptick.split)

lemma Aftertick_CHAOSSKIPS:
  ‹CHAOSSKIPS A R after✓ e =
   (case e of ✓(r) ⇒ Ω (CHAOSSKIPS A R) r
            | ev a ⇒ if a ∈ A then CHAOSSKIPS A R else Ψ (CHAOSSKIPS A R) a)›
  by (simp add: Aftertick_def After_CHAOSSKIPS split: eventptick.split)



lemma DF_FD_Aftertick:
  ‹DF A ⊑FD P ⟹ e ∈ P0 ⟹ DF A ⊑FD P after✓ e›
  by (cases e, simp add: Aftertick_def DF_FD_After)
    (metis anti_mono_initials_FD eventptick.distinct(1) image_iff initials_DF subsetD)

lemma DFSKIPS_FD_Aftertick:
  ‹DFSKIPS A R ⊑FD P ⟹ ev a ∈ P0 ⟹ DFSKIPS A R ⊑FD P after✓ ev a›
  by (simp add: Aftertick_def DFSKIPS_FD_After)



lemma deadlock_free_Aftertick:
  ‹e ∈ P0 ⟹ deadlock_free P ⟹
    deadlock_free (P after✓ e) ⟷
    (case e of ev a ⇒ True | ✓(r) ⇒ deadlock_free (Ω P r))›
  using deadlock_free_After by (auto simp add: Aftertick_def split: eventptick.split)

lemma deadlock_freeSKIPS_Aftertick:
  ‹e ∈ P0 ⟹ deadlock_freeSKIPS P ⟹
    deadlock_freeSKIPS (P after✓ e) ⟷
    (case e of ev a ⇒ True  | ✓(r) ⇒ deadlock_freeSKIPS (Ω P r))›
  using deadlock_freeSKIPS_After by (auto simp add: Aftertick_def split: eventptick.split)



subsection ‹Characterizations for Deadlock Freeness› 

lemma deadlock_free_imp_not_initial_tick: ‹deadlock_free P ⟹ range tick ∩ P0 = {}›
  by (rule ccontr, simp add: disjoint_iff)
    (meson anti_mono_initials_FD deadlock_free_def initial_tick_iff_FD_SKIP non_deadlock_free_SKIP subsetD)

lemma initial_tick_imp_range_ev_in_refusals: ‹✓(r) ∈ P0 ⟹ range ev ∈ ℛ P›
  unfolding initials_def image_def
  by (simp add: Refusals_iff is_processT6_TR_notin)

lemma deadlock_free_Aftertick_characterization: 
  ‹deadlock_free P ⟷ range ev ∉ ℛ P ∧ (∀e. ev e ∈ P0 ⟶ deadlock_free (P after✓ ev e))›
  (is ‹deadlock_free P ⟷ ?rhs›)
proof (intro iffI)
  from eventptick.exhaust_sel have ‹range ev = UNIV - range tick› by blast
  hence ‹range ev ∉ ℛ P ⟷ UNIV - range tick ∉ ℛ P› by metis
  thus ‹deadlock_free P ⟹ ?rhs›
    by (intro conjI)
      (solves ‹simp add: deadlock_free_F failure_refine_def,
                subst (asm) F_DF, auto simp add: Refusals_iff›,
        use DF_FD_Aftertick deadlock_free_def in blast)
next
  assume ‹?rhs›
  hence * : ‹range ev ∉ ℛ P›
    ‹ev e ∈ P0 ⟹ {(s, X) |s X. (ev e # s, X) ∈ ℱ P} ⊆ ℱ (DF UNIV)› for e
    by (simp_all add: deadlock_free_F failure_refine_def F_Aftertick subset_iff)
  show ‹deadlock_free P›
  proof (unfold deadlock_free_F failure_refine_def, safe)
    fix s X
    assume ** : ‹(s, X) ∈ ℱ P›
    show ‹(s, X) ∈ ℱ (DF UNIV)›
    proof (cases s)
      show ‹s = [] ⟹ (s, X) ∈ ℱ (DF UNIV)›
        by (subst F_DF, simp)
          (metis "*"(1) "**" Refusals_iff image_subset_iff is_processT4)
    next
      fix e s'
      assume *** : ‹s = e # s'›
      from "**"[THEN F_T, simplified this, THEN initials_memI]
        initial_tick_imp_range_ev_in_refusals "*"(1)
      obtain x where ‹e = ev x› ‹ev x ∈ P0›
        by (cases e) (simp_all add: initial_tick_imp_range_ev_in_refusals)
      with "*"(2)[OF this(2)] "**" "***" show ‹(s, X) ∈ ℱ (DF UNIV)›
        by (subst F_DF) (simp add: subset_iff)
    qed
  qed
qed



lemma deadlock_freeSKIPS_Aftertick_characterization: 
  ‹deadlock_freeSKIPS P ⟷ 
   UNIV ∉ ℛ P ∧ (∀e ∈ P0 - range tick. deadlock_freeSKIPS (P after✓ e))›
  (is ‹deadlock_freeSKIPS P ⟷ ?rhs›)
proof (intro iffI)
  show ?rhs if ‹deadlock_freeSKIPS P›
  proof (intro conjI)
    from ‹deadlock_freeSKIPS P› show ‹UNIV ∉ ℛ P›
      by (simp add: deadlock_freeSKIPS_def failure_refine_def)
        (subst (asm) F_DFSKIPS, auto simp add: Refusals_iff)
  next
    from ‹deadlock_freeSKIPS P› show ‹∀e∈P0 - range tick. deadlock_freeSKIPS (P after✓ e)›
      by (auto simp add: deadlock_freeSKIPS_Aftertick split: eventptick.split)
  qed
next
  assume assm : ‹?rhs›
  have * : ‹ev e ∈ P0 ⟹ {(s, X) |s X. (ev e # s, X) ∈ ℱ P} ⊆ ℱ (DFSKIPS UNIV UNIV)› for e
    using assm[THEN conjunct2, rule_format, of ‹ev e›, simplified]
    by (simp add: deadlock_freeSKIPS_def failure_refine_def F_Aftertick image_iff)
  show ‹deadlock_freeSKIPS P›
  proof (unfold deadlock_freeSKIPS_def failure_refine_def, safe)
    fix s X
    assume ** : ‹(s, X) ∈ ℱ P›
    show ‹(s, X) ∈ ℱ (DFSKIPS UNIV UNIV)›
    proof (cases s)
      from assm[THEN conjunct1] "**" show ‹s = [] ⟹ (s, X) ∈ ℱ (DFSKIPS UNIV UNIV)›
        by (subst F_DFSKIPS, simp add: Refusals_iff)
          (metis UNIV_eq_I eventptick.exhaust)
    next
      fix e s'
      assume *** : ‹s = e # s'›
      show ‹(s, X) ∈ ℱ (DFSKIPS UNIV UNIV)›
      proof (cases e)
        fix a assume ‹e = ev a›
        with "**" "***" initials_memI F_T have ‹ev a ∈ P0› by blast
        with "*"[OF this] "**" "***" ‹e = ev a› show ‹(s, X) ∈ ℱ (DFSKIPS UNIV UNIV)›
          by (subst F_DFSKIPS) (simp add: subset_iff)
      next
        fix r assume ‹e = ✓(r)›
        hence ‹s = [✓(r)]›
          by (metis "**" "***" eventptick.disc(2) front_tickFree_Cons_iff is_processT2)
        thus ‹(s, X) ∈ ℱ (DFSKIPS UNIV UNIV)›
          by (subst F_DFSKIPS, simp)
      qed
    qed
  qed
qed



subsection ‹Continuity›

lemma Aftertick_cont [simp] : 
  assumes cont_ΨΩ : ‹case e of ev a ⇒ cont (λP. Ψ P a) | ✓(r) ⇒ cont (λP. Ω P r)›
    and cont_f : ‹cont f›
  shows ‹cont (λx. f x after✓ e)›
  by (cases e, simp_all add: Aftertick_def)
    (use After_cont cont_ΨΩ cont_f in ‹auto intro: cont_compose›)



end


(*<*)
end
  (*>*)