Theory After_Trace_Operator

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

section‹ The After trace Operator ›

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


context AfterExt
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, 'r) eventptick›}.
      Since a trace of a term‹P› is just an typ‹('a, 'r) eventptick list›, the following 
      inductive definition is natural.›

fun Aftertrace :: ‹('a, 'r) processptick ⇒ ('a, 'r) traceptick ⇒ ('a, 'r) processptick› (infixl ‹after𝒯› 86)
  where ‹P after𝒯 [] = P›
  |     ‹P after𝒯 (e # t) = P after✓ e after𝒯 t›



text ‹We can also induct backward.›

lemma Aftertrace_append: ‹P after𝒯 (t @ u) = P after𝒯 t after𝒯 u›
  apply (induct u rule: rev_induct, solves ‹simp›)
  apply (induct t rule: rev_induct, solves ‹simp›)
  by (metis Aftertrace.simps append.assoc append.right_neutral append_Cons append_Nil)

lemma Aftertrace_snoc : ‹P after𝒯 (t @ [e]) = P after𝒯 t after✓ e›
  by (simp add: Aftertrace_append)



subsection ‹Projections›

lemma F_Aftertrace:
  ‹tF t ⟹ (t @ u, X) ∈ ℱ P ⟹ (u, X) ∈ ℱ (P after𝒯 t)›
proof (induct t arbitrary: u rule: rev_induct)
  show ‹([] @ u, X) ∈ ℱ P ⟹ (u, X) ∈ ℱ (P after𝒯 [])› for u by simp
next
  fix e t u
  assume   hyp : ‹tF t ⟹ (t @ u, X) ∈ ℱ P ⟹ (u, X) ∈ ℱ (P after𝒯 t)› for u
  assume prems : ‹tF (t @ [e])› ‹((t @ [e]) @ u, X) ∈ ℱ P›
  have * : ‹(e # u, X) ∈ ℱ (P after𝒯 t)› by (rule hyp; use prems in simp)
  thus ‹(u, X) ∈ ℱ (P after𝒯 (t @ [e]))›
    by (simp add: Aftertrace_snoc F_Aftertick split: eventptick.split)
      (metis initials_memI F_T non_tickFree_tick prems(1) tickFree_append_iff)
qed


lemma D_Aftertrace:
  ‹tF t ⟹ t @ u ∈ 𝒟 P ⟹ u ∈ 𝒟 (P after𝒯 t)›
proof (induct t arbitrary: u rule: rev_induct)
  show ‹[] @ u ∈ 𝒟 P ⟹ u ∈ 𝒟 (P after𝒯 [])› for u by simp
next
  fix e t u
  assume   hyp : ‹tF t ⟹ t @ u ∈ 𝒟 P ⟹ u ∈ 𝒟 (P after𝒯 t)› for u
  assume prems : ‹tF ((t @ [e]))› ‹(t @ [e]) @ u ∈ 𝒟 P›
  have * : ‹e # u ∈ 𝒟 (P after𝒯 t)› by (rule hyp; use prems in simp)
  thus ‹u ∈ 𝒟 (P after𝒯 (t @ [e]))›
    by (simp add: Aftertrace_snoc D_Aftertick split: eventptick.split)
      (metis initials_memI D_T non_tickFree_tick prems(1) tickFree_append_iff)
qed


lemma T_Aftertrace : ‹t @ u ∈ 𝒯 P ⟹ u ∈ 𝒯 (P after𝒯 t)›
proof (induct t arbitrary: u rule: rev_induct)
  show ‹[] @ u ∈ 𝒯 P ⟹ u ∈ 𝒯 (P after𝒯 [])› for u by simp
next
  fix e t u
  assume  hyp : ‹t @ u ∈ 𝒯 P ⟹ u ∈ 𝒯 (P after𝒯 t)› for u
  assume prem : ‹(t @ [e]) @ u ∈ 𝒯 P›
  have * : ‹e # u ∈ 𝒯 (P after𝒯 t)› by (rule hyp, use prem in simp)
  thus ‹u ∈ 𝒯 (P after𝒯 (t @ [e]))›
    by (simp add: Aftertrace_snoc T_Aftertick split: eventptick.split)
      (metis initials_memI append_T_imp_tickFree
        is_processT1_TR non_tickFree_tick prem tickFree_append_iff)
qed


corollary initials_Aftertrace :
  ‹t @ e # u ∈ 𝒯 P ⟹ e ∈ (P after𝒯 t)0›
  by (metis initials_memI T_Aftertrace)

corollary F_imp_R_Aftertrace: ‹tF t ⟹ (t, X) ∈ ℱ P ⟹ X ∈ ℛ (P after𝒯 t)›
  by (simp add: F_Aftertrace Refusals_iff)

corollary D_imp_Aftertrace_is_BOT: ‹tF t ⟹ t ∈ 𝒟 P ⟹ P after𝒯 t = ⊥›
  by (simp add: BOT_iff_Nil_D D_Aftertrace)


lemma F_Aftertrace_eq:
  ‹t ∈ 𝒯 P ⟹ tF t ⟹ ℱ (P after𝒯 t) = {(u, X). (t @ u, X) ∈ ℱ P}›
proof safe
  show ‹t ∈ 𝒯 P ⟹ tF t ⟹ (u, X) ∈ ℱ (P after𝒯 t) ⟹ (t @ u, X) ∈ ℱ P› for u X
  proof (induct t arbitrary: u rule: rev_induct)
    show ‹(u, X) ∈ ℱ (P after𝒯 []) ⟹ ([] @ u, X) ∈ ℱ P› for u by simp
  next
    case (snoc e t)
    from initials_Aftertrace snoc.prems(1) have * : ‹e ∈ (P after𝒯 t)0› by blast
    obtain a where ‹e = ev a› 
      by (metis eventptick.exhaust non_tickFree_tick snoc.prems(2) tickFree_append_iff)
    show ?case
      apply (simp, rule snoc.hyps)
        apply (metis prefixI is_processT3_TR snoc.prems(1))
       apply (use snoc.prems(2) tickFree_append_iff in blast)
      using snoc.prems(3) "*" by (simp add: Aftertrace_snoc F_Aftertick ‹e = ev a›)
  qed
next
  show ‹tF t ⟹ (t @ u, X) ∈ ℱ P ⟹ (u, X) ∈ ℱ (P after𝒯 t)› for u X
    by (fact F_Aftertrace)
qed


lemma D_Aftertrace_eq:
  ‹t ∈ 𝒯 P ⟹ tF t ⟹ 𝒟 (P after𝒯 t) = {u. t @ u ∈ 𝒟 P}›
proof safe
  show ‹t ∈ 𝒯 P ⟹ tF t ⟹ u ∈ 𝒟 (P after𝒯 t) ⟹ t @ u ∈ 𝒟 P› for u
  proof (induct t arbitrary: u rule: rev_induct)
    show ‹u ∈ 𝒟 (P after𝒯 []) ⟹ [] @ u ∈ 𝒟 P› for u by simp
  next
    case (snoc e t)
    from initials_Aftertrace snoc.prems(1) have * : ‹e ∈ (P after𝒯 t)0› by blast
    obtain a where ‹e = ev a› 
      by (metis eventptick.exhaust non_tickFree_tick snoc.prems(2) tickFree_append_iff)
    show ?case
      apply (simp, rule snoc.hyps)
        apply (metis prefixI is_processT3_TR snoc.prems(1))
      using "*" Aftertick_def Aftertrace_snoc D_After ‹e = ev a› snoc.prems(2, 3) by auto
  qed
next
  show ‹tF t ⟹ t @ u ∈ 𝒟 P ⟹ u ∈ 𝒟 (P after𝒯 t)› for u by (fact D_Aftertrace)
qed


lemma T_Aftertrace_eq:
  ‹t ∈ 𝒯 P ⟹ tF t ⟹ 𝒯 (P after𝒯 t) = {u. t @ u ∈ 𝒯 P}›
proof safe
  show ‹t ∈ 𝒯 P ⟹ tF t ⟹ u ∈ 𝒯 (P after𝒯 t) ⟹ t @ u ∈ 𝒯 P› for u
  proof (induct t arbitrary: u rule: rev_induct)
    show ‹u ∈ 𝒯 (P after𝒯 []) ⟹ [] @ u ∈ 𝒯 P› for u by simp
  next
    case (snoc e t)
    from initials_Aftertrace snoc.prems(1) have * : ‹e ∈ (P after𝒯 t)0› by blast
    obtain a where ‹e = ev a› 
      by (metis eventptick.exhaust non_tickFree_tick snoc.prems(2) tickFree_append_iff)
    show ?case
      apply (simp, rule snoc.hyps)
        apply (meson prefixI is_processT3_TR snoc.prems(1))
      using "*" Aftertick_def Aftertrace_snoc T_After ‹e = ev a› snoc.prems(2, 3) by auto
  qed
next
  show ‹t @ u ∈ 𝒯 P ⟹ u ∈ 𝒯 (P after𝒯 t)› for u by (fact T_Aftertrace)
qed



subsection ‹Monotony›

(* lemma mono_Aftertrace_T  :
  ‹(⋀P Q. P ⊑T Q ⟹ Ω P ⊑T Ω Q)  ⟹ P ⊑T Q  ⟹ P after𝒯 s ⊑T Q after𝒯 s›
  and mono_Aftertrace_F  :
  ‹(⋀P Q. P ⊑F Q ⟹ Ω P ⊑F Ω Q)  ⟹ P ⊑F Q  ⟹ P after𝒯 s ⊑F Q after𝒯 s›
  and mono_Aftertrace_D  :
  ‹(⋀P Q. P ⊑D Q ⟹ Ω P ⊑D Ω Q)  ⟹ P ⊑D Q  ⟹ P after𝒯 s ⊑D Q after𝒯 s›
  and mono_Aftertrace_FD :
  ‹(⋀P Q. P ⊑FD Q ⟹ Ω P ⊑FD Ω Q) ⟹ P ⊑FD Q ⟹ P after𝒯 s ⊑FD Q after𝒯 s›
  and mono_Aftertrace_DT :
  ‹(⋀P Q. P ⊑DT Q ⟹ Ω P ⊑DT Ω Q) ⟹ P ⊑DT Q ⟹ P after𝒯 s ⊑DT Q after𝒯 s›
  if ‹s ∈ 𝒯 Q› and ‹tF s›
  using that apply (all ‹induct s arbitrary: P Q rule: rev_induct; simp add: Aftertrace_snoc›)

  oops
      *)

(* lemma mono_Aftertrace : ‹P ⊑ Q ⟹ P after𝒯 s ⊑ Q after𝒯 s›
  by (induct s rule: rev_induct) (simp_all add: mono_Aftertick Aftertrace_snoc)

lemma mono_Aftertrace_T : 
  ‹P ⊑T Q ⟹ s ∈ 𝒯 Q ⟹ tF s ⟹ P after𝒯 s ⊑T Q after𝒯 s›
  by (induct s rule: rev_induct; simp add: Aftertrace_snoc)
     (rule mono_Aftertick_T; use is_processT3_ST in blast)

lemma mono_Aftertrace_F : 
  ‹P ⊑F Q ⟹ s ∈ 𝒯 Q ⟹ tF s ⟹ P after𝒯 s ⊑F Q after𝒯 s›
  by (induct s rule: rev_induct; simp add: Aftertrace_snoc)
     (metis eventptick.exhaust is_processT3_ST mono_Aftertick_F initials_Aftertrace)

lemma mono_Aftertrace_D : ‹P ⊑D Q ⟹ P after𝒯 s ⊑D Q after𝒯 s›
  by (induct s rule: rev_induct) (simp_all add: mono_Aftertick_D Aftertrace_snoc)

lemma mono_Aftertrace_FD :
  ‹P ⊑FD Q ⟹ s ∈ 𝒯 Q ⟹ P after𝒯 s ⊑FD Q after𝒯 s›
  by (induct s rule: rev_induct; simp add: Aftertrace_snoc)
     (meson initials_memI T_Aftertrace is_processT3_ST mono_Aftertick_FD)

lemma mono_Aftertrace_DT :
  ‹P ⊑DT Q ⟹ P after𝒯 s ⊑DT Q after𝒯 s›
  by (induct s rule: rev_induct; simp add: Aftertrace_snoc mono_Aftertick_DT)

 *)




subsection ‹Four inductive Constructions with @{const [source] Aftertrace}›

subsubsection ‹Reachable Processes›

inductive_set reachable_processes :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick set› (‹ℛproc›)
  for P :: ‹('a, 'r) processptick›
  where reachable_self : ‹P ∈ ℛproc P›
  |     reachable_after: ‹Q ∈ ℛproc P ⟹ ev e ∈ Q0 ⟹ Q after e ∈ ℛproc P›


lemma reachable_processes_is: ‹ℛproc P = {Q. ∃t ∈ 𝒯 P. tF t ∧ Q = P after𝒯 t}›
proof safe
  show ‹Q ∈ ℛproc P ⟹ ∃t ∈ 𝒯 P. tF t ∧ Q = P after𝒯 t› for Q
  proof (induct rule: reachable_processes.induct)
    show ‹∃t ∈ 𝒯 P. tF t ∧ P = P after𝒯 t›
    proof (intro bexI)
      show ‹tF [] ∧ P = P after𝒯 []› by simp
    next
      show ‹[] ∈ 𝒯 P› by simp
    qed
  next
    fix Q e
    assume assms : ‹Q ∈ ℛproc P› ‹∃t ∈ 𝒯 P. tF t ∧ Q = P after𝒯 t› ‹ev e ∈ Q0›
    from assms(2) obtain t where * : ‹tF t› ‹t ∈ 𝒯 P› ‹Q = P after𝒯 t› by blast
    show ‹∃t∈𝒯 P. tF t ∧ Q after e = P after𝒯 t›
    proof (intro bexI)
      show ‹tF (t @ [ev e]) ∧ Q after e = P after𝒯 (t @ [ev e])›
        by (simp add: Aftertrace_snoc Aftertick_def "*"(1, 3))
    next
      from "*" T_Aftertrace_eq assms(3) initials_def
      show ‹t @ [ev e] ∈ 𝒯 P› by fastforce
    qed
  qed
next
  show ‹t ∈ 𝒯 P ⟹ tF t ⟹ P after𝒯 t ∈ ℛproc P› for t
  proof (induct t rule: rev_induct)
    show ‹P after𝒯 [] ∈ ℛproc P› by (simp add: reachable_self)
  next
    fix t e
    assume   hyp : ‹t ∈ 𝒯 P ⟹ tF t ⟹ P after𝒯 t ∈ ℛproc P›
      and prems : ‹t @ [e] ∈ 𝒯 P› ‹tF (t @ [e])›
    from prems T_F_spec is_processT3 tickFree_append_iff
    have * : ‹t ∈ 𝒯 P› ‹tF t› by blast+
    obtain a where ‹e = ev a› 
      by (metis eventptick.exhaust non_tickFree_tick prems(2) tickFree_append_iff)
    thus ‹P after𝒯 (t @ [e]) ∈ ℛproc P›
      by (simp add: Aftertrace_snoc Aftertick_def)
        (use initials_Aftertrace prems(1) in
          ‹blast intro: initials_Aftertrace prems(1) reachable_after[OF hyp[OF "*"]]›)
  qed
qed

lemma reachable_processes_trans: ‹Q ∈ ℛproc P ⟹ R ∈ ℛproc Q ⟹ R ∈ ℛproc P›
  apply (simp add: reachable_processes_is, elim bexE)
  apply (simp add: Aftertrace_append[symmetric] T_Aftertrace_eq)
  using tickFree_append_iff by blast



subsubsection ‹Antecedent Processes›

inductive_set antecedent_processes :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick set› (‹𝒜proc›)
  for P :: ‹('a, 'r) processptick›
  where antecedent_self : ‹P ∈ 𝒜proc P›
  |     antecedent_after: ‹Q after e ∈ 𝒜proc P ⟹ ev e ∈ Q0 ⟹ Q ∈ 𝒜proc P›


lemma antecedent_processes_is: ‹𝒜proc P = {Q. ∃t ∈ 𝒯 Q. tF t ∧ P = Q after𝒯 t}›
proof safe
  have ‹Q ∈ 𝒜proc P ⟹ P ∈ ℛproc Q› for Q
  proof (induct rule: antecedent_processes.induct)
    show ‹P ∈ ℛproc P› by (fact reachable_self)
  next
    show ‹Q after e ∈ 𝒜proc P ⟹ P ∈ ℛproc (Q after e) ⟹ ev e ∈ Q0 ⟹ P ∈ ℛproc Q› for Q e
      by (meson reachable_after reachable_self reachable_processes_trans)
  qed
  thus ‹Q ∈ 𝒜proc P ⟹ ∃t ∈ 𝒯 Q. tF t ∧ P = Q after𝒯 t› for Q 
    by (simp add: reachable_processes_is)
next
  show ‹t ∈ 𝒯 Q ⟹ tF t ⟹ Q ∈ 𝒜proc (Q after𝒯 t)› for t Q
  proof (induct t arbitrary: Q)
    show ‹Q ∈ 𝒜proc (Q after𝒯 [])› for Q by (simp add: antecedent_self)
  next
    fix e t Q
    assume   hyp : ‹⋀Q. t ∈ 𝒯 Q ⟹ tF t ⟹ Q ∈ 𝒜proc (Q after𝒯 t)›
      and prems : ‹e # t ∈ 𝒯 Q› ‹tF (e # t)›
    from prems obtain a where ‹e = ev a› ‹ev a ∈ Q0›
      by (metis initials_memI is_ev_def tickFree_Cons_iff)
    with prems have ‹t ∈ 𝒯 (Q after a)› ‹tF t› by (simp_all add: T_After)
    from hyp[OF this] have ‹Q after a ∈ 𝒜proc (Q after𝒯 (e # t))›
      by (simp add: Aftertick_def ‹e = ev a›)
    from this ‹ev a ∈ Q0› show ‹Q ∈ 𝒜proc (Q after𝒯 (e # t))›
      by (fact antecedent_after)
  qed
qed

lemma antecedent_processes_trans: ‹Q ∈ 𝒜proc P ⟹ R ∈ 𝒜proc Q ⟹ R ∈ 𝒜proc P›
  apply (simp add: antecedent_processes_is, elim bexE)
  apply (simp add: Aftertrace_append[symmetric] T_Aftertrace_eq)
  using tickFree_append_iff by blast


corollary antecedent_processes_iff_rev_reachable_processes: ‹P ∈ 𝒜proc Q ⟷ Q ∈ ℛproc P›
  by (simp add: antecedent_processes_is reachable_processes_is)


subsection ‹Nth initials Events›

primrec nth_initials :: ‹('a, 'r) processptick ⇒ nat ⇒ ('a, 'r) eventptick set› (‹_⇗_⇖› [1000, 3] 999)
  where ‹P⇗0⇖     = P0›
  |     ‹P⇗Suc n⇖ = ⋃ {(P after e)⇗n⇖ |e. ev e ∈ P0}›


lemma ‹P⇗0⇖ = P0› by simp

lemma  first_initials_is : ‹P⇗1⇖ = ⋃ {(P after e)0 |e. ev e ∈ P0}› by simp

lemma second_initials_is :
  ‹P⇗2⇖ = ⋃ {(P after e after f)0 |e f. ev e ∈ P0 ∧ ev f ∈ (P after e)0}› 
  by (auto simp add: numeral_eq_Suc)

lemma third_initials_is :
  ‹P⇗3⇖ = ⋃ {(P after e after f after g)0 |e f g. 
              ev e ∈ P0 ∧ ev f ∈ (P after e)0 ∧ ev g ∈ (P after e after f)0}› 
  by (auto simp add: numeral_eq_Suc)


text ‹More generally, we have the following result.›

lemma nth_initials_is: ‹P⇗n⇖ = ⋃ {(P after𝒯 t)0 | t. t ∈ 𝒯 P ∧ tF t ∧ length t = n}›
proof (induct n arbitrary: P)
  show ‹P⇗0⇖ = ⋃ {(P after𝒯 t)0 |t. t ∈ 𝒯 P ∧ tF t ∧ length t = 0}› for P  by simp
next
  fix n P
  assume hyp : ‹P⇗n⇖ = ⋃ {(P after𝒯 t)0 |t. t ∈ 𝒯 P ∧ tF t ∧ length t = n}› for P
  show ‹P⇗Suc n⇖ = ⋃ {(P after𝒯 t)0 |t. t ∈ 𝒯 P ∧ tF t ∧ length t = Suc n}›
  proof safe
    show ‹e ∈ P⇗Suc n⇖ ⟹ e ∈ ⋃ {(P after𝒯 t)0 |t. t ∈ 𝒯 P ∧ tF t ∧ length t = Suc n}› for e
      by (auto simp add: hyp T_After)
        (metis (no_types, lifting) AfterExt.Aftertick_def AfterExt.Aftertrace.simps(2)
          eventptick.simps(5) is_ev_def length_Cons tickFree_Cons_iff)
  next
    fix e t
    assume assms : ‹e ∈ (P after𝒯 t)0› ‹t ∈ 𝒯 P› ‹tF t› ‹length t = Suc n›
    from assms(1-3) have * : ‹t @ [e] ∈ 𝒯 P›
      unfolding initials_def by (simp add: T_Aftertrace_eq)
    from assms(3, 4)obtain a t' where ** : ‹t = ev a # t'› ‹tF t'› ‹length t' = n›
      by (metis Suc_length_conv eventptick.collapse(1) tickFree_Cons_iff)
    with initials_memI assms(2) have ‹ev a ∈ P0› by blast
    show ‹e ∈ P⇗Suc n⇖›
    proof (unfold nth_initials.simps(2), rule UnionI)
      from ‹ev a ∈ P0› show ‹(P after a)⇗n⇖ ∈ {(P after e)⇗n⇖ |e. ev e ∈ P0}› by blast
    next
      from assms(1, 2) "**"(1-3) ‹ev a ∈ P0›
      show ‹e ∈ (P after a)⇗n⇖› by (auto simp add: hyp "**"(1) Aftertick_def T_After)
    qed
  qed
qed


lemma nth_initials_DF: ‹(DF A)⇗n⇖ = ev ` A›
  by (induct n) (auto simp add: initials_DF After_DF)

lemma nth_initials_DFSKIPS:
  ‹(DFSKIPS A R)⇗n⇖ = (if A = {} then if n = 0 then tick ` R else {} else ev ` A ∪ tick ` R)›
  by (induct n) (auto simp add: initials_DFSKIPS After_DFSKIPS)

lemma nth_initials_RUN: ‹(RUN A)⇗n⇖ = ev ` A›
  by (induct n) (auto simp add: initials_RUN After_RUN)

lemma nth_initials_CHAOS: ‹(CHAOS A)⇗n⇖ = ev ` A›
  by (induct n) (auto simp add: initials_CHAOS After_CHAOS)

lemma nth_initials_CHAOSSKIPS:
  ‹(CHAOSSKIPS A R)⇗n⇖ = (if A = {} then if n = 0 then tick ` R else {} else ev ` A ∪ tick ` R)›
  by (induct n) (auto simp add: initials_CHAOSSKIPS After_CHAOSSKIPS)



subsubsection ‹Reachable Ev›

inductive reachable_ev :: ‹('a, 'r) processptick ⇒ 'a ⇒ bool›
  where initial_ev_reachable:
    ‹ev a ∈ P0 ⟹ reachable_ev P a›
  |     reachable_ev_after_reachable:
    ‹ev b ∈ P0 ⟹ reachable_ev (P after b) a ⟹ reachable_ev P a›

definition reachable_ev_set :: ‹('a, 'r) processptick ⇒ 'a set› (‹ℛev›)
  where ‹ℛev P ≡ ⋃Q ∈ ℛproc P. {a. ev a ∈ Q0}›


lemma reachable_ev_BOT : ‹reachable_ev ⊥ a›
  and not_reachable_ev_STOP : ‹¬ reachable_ev STOP a›
  and not_reachable_ev_SKIP : ‹¬ reachable_ev (SKIP r) a›
  by (subst reachable_ev.simps, simp)+


lemma events_of_iff_reachable_ev: ‹a ∈ α(P) ⟷ reachable_ev P a›
proof (intro iffI)
  show ‹reachable_ev P a ⟹ a ∈ α(P)›
    apply (induct rule: reachable_ev.induct;
        simp add: T_After events_of_def initials_def split: if_split_asm)
    by (meson list.set_intros(1)) (meson list.set_intros(2))
next
  assume ‹a ∈ α(P)›
  then obtain t where * : ‹t ∈ 𝒯 P› ‹ev a ∈ set t› by (meson events_of_memD)
  thus ‹reachable_ev P a›
  proof (induct t arbitrary: P)
    show ‹⋀P a. ev a ∈ set [] ⟹ reachable_ev P a› by simp
  next
    case (Cons e t)
    from Cons.prems(1) initials_memI
    have * : ‹e ∈ P0› unfolding initials_def by blast
    from Cons.prems(2) consider ‹e = ev a› | ‹ev a ∈ set t› by auto
    thus ‹reachable_ev P a›
    proof cases
      assume ‹e = ev a›
      from "*"[simplified this]
      show ‹reachable_ev P a› by (fact reachable_ev.intros(1))
    next
      show ‹reachable_ev P a› if ‹ev a ∈ set t›
      proof (cases e)
        fix b
        assume ‹e = ev b›
        with * Cons.prems(1) have ‹t ∈ 𝒯 (P after b)› by (force simp add: T_After)
        show ‹reachable_ev P a›
        proof (rule reachable_ev.intros(2))
          from "*" ‹e = ev b› show ‹ev b ∈ P0› by blast
        next
          show ‹reachable_ev (P after b) a›
            by (fact Cons.hyps[OF ‹t ∈ 𝒯 (P after b)› ‹ev a ∈ set t›])
        qed
      next
        from Cons.prems(1) have ‹e = ✓(r) ⟹ t = []› for r
          by simp (meson T_imp_front_tickFree eventptick.disc(2) front_tickFree_Cons_iff)
        with ‹ev a ∈ set t› show ‹e = ✓(r) ⟹ reachable_ev P a› for r by simp
      qed
    qed
  qed
qed


lemma reachable_ev_iff_in_initials_Aftertrace_for_some_tickFree_T:
  ‹reachable_ev P a ⟷ (∃t ∈ 𝒯 P. tF t ∧ ev a ∈ (P after𝒯 t)0)›
proof (intro iffI)                                          
  show ‹reachable_ev P a ⟹ ∃t∈𝒯 P. tF t ∧ ev a ∈ (P after𝒯 t)0›
  proof (induct rule: reachable_ev.induct)
    show ‹ev a ∈ P0 ⟹ ∃t∈𝒯 P. tF t ∧ ev a ∈ (P after𝒯 t)0› for a P
    proof (intro bexI)
      show ‹ev a ∈ P0 ⟹ tF [] ∧ ev a ∈ (P after𝒯 [])0› by simp
    next
      show ‹[] ∈ 𝒯 P› by (fact Nil_elem_T)
    qed
  next
    fix b a P
    assume prems : ‹ev b ∈ P0› ‹reachable_ev (P after b) a›
      and   hyp : ‹∃t ∈ 𝒯 (P after b). tF t ∧ ev a ∈ (P after b after𝒯 t)0›
    from hyp obtain t
      where * : ‹tF t› ‹t ∈ 𝒯 (P after b)›
        ‹ev a ∈ (P after b after𝒯 t)0› by blast
    show ‹∃t ∈ 𝒯 P. tF t ∧ ev a ∈ (P after𝒯 t)0›
    proof (intro bexI)
      show ‹tF (ev b # t) ∧ ev a ∈ (P after𝒯 (ev b # t))0›
        by (simp add: "*"(1, 3) Aftertick_def)        
    next
      from "*"(2) show ‹ev b # t ∈ 𝒯 P› by (simp add: T_After prems(1))
    qed
  qed
next
  show ‹∃t ∈ 𝒯 P. tF t ∧ ev a ∈ (P after𝒯 t)0 ⟹ reachable_ev P a›
  proof (elim bexE conjE)
    show ‹t ∈ 𝒯 P ⟹ tF t ⟹ ev a ∈ (P after𝒯 t)0 ⟹ reachable_ev P a› for t
    proof (induct t arbitrary: P)
      show ‹ev a ∈ (P after𝒯 [])0 ⟹ reachable_ev P a› for P
        by (simp add: reachable_ev.intros(1))
    next
      fix e t P
      assume   hyp : ‹t ∈ 𝒯 P ⟹ tF t ⟹ ev a ∈ (P after𝒯 t)0 ⟹
                      reachable_ev P a› for P
      assume prems : ‹tF (e # t)› ‹e # t ∈ 𝒯 P› ‹ev a ∈ (P after𝒯 (e # t))0›
      from prems(1) obtain b where ‹e = ev b› by (cases e; simp)
      with prems(2) have initial : ‹ev b ∈ P0› by (simp add: initials_memI)
      from reachable_ev_after_reachable[OF initial[simplified ‹e = ev b›]]
        Aftertick_def T_After ‹e = ev b› hyp prems initial
      show ‹reachable_ev P a› by auto
    qed
  qed
qed



subsubsection ‹Properties›

corollary reachable_ev_set_is_mem_Collect_reachable_ev:
  ‹ℛev P = {a. reachable_ev P a}›
  by (auto simp add: reachable_ev_set_def reachable_processes_is
      reachable_ev_iff_in_initials_Aftertrace_for_some_tickFree_T)  

corollary events_of_is_reachable_ev_set: ‹α(P) = ℛev P›
  by (simp add: reachable_ev_set_is_mem_Collect_reachable_ev
      set_eq_iff events_of_iff_reachable_ev)

lemma events_of_reachable_processes_subset: ‹Q ∈ ℛproc P ⟹ α(Q) ⊆ α(P)›
  by (induct rule: reachable_processes.induct)
    (simp_all add: subset_iff events_of_iff_reachable_ev reachable_ev_after_reachable)


corollary events_of_antecedent_processes_superset: ‹Q ∈ 𝒜proc P ⟹ α(P) ⊆ α(Q)›
  by (simp add: antecedent_processes_iff_rev_reachable_processes
      events_of_reachable_processes_subset)

lemma events_of_is_Union_nth_initials: ‹α(P) = (⋃n. {a. ev a ∈ P⇗n⇖})›
  by (auto simp add: nth_initials_is events_of_iff_reachable_ev
      reachable_ev_iff_in_initials_Aftertrace_for_some_tickFree_T)+


subsubsection ‹Reachable Tick›

inductive reachable_tick :: ‹('a, 'r) processptick ⇒ 'r ⇒ bool›
  where initial_tick_reachable:
    ‹✓(r) ∈ P0 ⟹ reachable_tick P r›
  |     reachable_tick_after_reachable:
    ‹ev a ∈ P0 ⟹ reachable_tick (P after a) r ⟹ reachable_tick P r›

definition reachable_tick_set :: ‹('a, 'r) processptick ⇒ 'r set› (‹ℛ✓›)
  where ‹ℛ✓ P ≡ ⋃Q ∈ ℛproc P. {r. ✓(r) ∈ Q0}›


lemma reachable_tick_BOT : ‹reachable_tick ⊥ r›
  and not_reachable_tick_STOP : ‹¬ reachable_tick STOP s›
  and reachable_tick_SKIP_iff : ‹reachable_tick (SKIP r) s ⟷ s = r›
  by (subst reachable_tick.simps, simp)+


lemma ticks_of_iff_reachable_tick : ‹r ∈ ✓s(P) ⟷ reachable_tick P r›
proof (intro iffI)
  show ‹reachable_tick P r ⟹ r ∈ ✓s(P)›
    apply (induct rule: reachable_tick.induct;
        simp add: T_After ticks_of_def initials_def split: if_split_asm)
    by (metis append_Nil, metis append_Cons)
next
  assume ‹r ∈ ✓s(P)›
  then obtain t where * : ‹t @ [✓(r)] ∈ 𝒯 P› by (meson ticks_of_memD)
  thus ‹reachable_tick P r›
  proof (induct t arbitrary: P)
    show ‹[] @ [✓(r)] ∈ 𝒯 P ⟹ reachable_tick P r› for P
      by (simp add: initial_tick_reachable initials_memI)
  next
    case (Cons e t)
    obtain a where ‹e = ev a›
      by (meson Cons.prems append_T_imp_tickFree is_ev_def not_Cons_self2 tickFree_Cons_iff)
    moreover from Cons.prems have ‹e ∈ P0› by (auto intro: initials_memI)
    ultimately have ‹t @ [✓(r)] ∈ 𝒯 (P after a)›
      using Cons.prems by (simp add: T_After ‹e = ev a›)
    with Cons.hyps have ‹reachable_tick (P after a) r› by blast
    with ‹e = ev a› ‹e ∈ P0› reachable_tick_after_reachable
    show ‹reachable_tick P r› by blast
  qed
qed


lemma reachable_tick_iff_in_initials_Aftertrace_for_some_tickFree_T:
  ‹reachable_tick P r ⟷ (∃t ∈ 𝒯 P. tF t ∧ ✓(r) ∈ (P after𝒯 t)0)›
proof (intro iffI)                                      
  show ‹reachable_tick P r ⟹ ∃t∈𝒯 P. tF t ∧ ✓(r) ∈ (P after𝒯 t)0›
  proof (induct rule: reachable_tick.induct)
    show ‹✓(r) ∈ P0 ⟹ ∃t∈𝒯 P. tF t ∧ ✓(r) ∈ (P after𝒯 t)0› for r P
    proof (intro bexI)
      show ‹✓(r) ∈ P0 ⟹ tF [] ∧ ✓(r) ∈ (P after𝒯 [])0› by simp
    next
      show ‹[] ∈ 𝒯 P› by (fact Nil_elem_T)
    qed
  next
    fix a P r
    assume prems : ‹ev a ∈ P0› ‹reachable_tick (P after a) r›
      and   hyp : ‹∃t∈𝒯 (P after a). tF t ∧ ✓(r) ∈ (P after a after𝒯 t)0›
    from hyp obtain t
      where * : ‹tF t› ‹t ∈ 𝒯 (P after a)›
        ‹✓(r) ∈ (P after a after𝒯 t)0› by blast
    show ‹∃t∈𝒯 P. tF t ∧ ✓(r) ∈ (P after𝒯 t)0›
    proof (intro bexI)
      show ‹tF (ev a # t) ∧ ✓(r) ∈ (P after𝒯 (ev a # t))0›
        by (simp add: "*"(1, 3) Aftertick_def)        
    next
      from "*"(2) show ‹ev a # t ∈ 𝒯 P› by (simp add: T_After prems(1))
    qed
  qed
next
  show ‹ ∃t∈𝒯 P. tF t ∧ ✓(r) ∈ (P after𝒯 t)0 ⟹ reachable_tick P r›
  proof (elim bexE conjE)
    show ‹t ∈ 𝒯 P ⟹ tF t ⟹ ✓(r) ∈ (P after𝒯 t)0 ⟹ reachable_tick P r› for t
    proof (induct t arbitrary: P)
      show ‹✓(r) ∈ (P after𝒯 [])0 ⟹ reachable_tick P r› for P
        by (simp add: initial_tick_reachable)
    next
      fix e t P
      assume   hyp : ‹t ∈ 𝒯 P ⟹ tF t ⟹ ✓(r) ∈ (P after𝒯 t)0 ⟹ reachable_tick P r› for P
      assume prems : ‹tF (e # t)› ‹e # t ∈ 𝒯 P› ‹✓(r) ∈ (P after𝒯 (e # t))0›
      from prems(1) obtain a where ‹e = ev a› by (cases e; simp)
      with prems(2) have initial : ‹ev a ∈ P0› by (simp add: initials_memI)
      from reachable_tick_after_reachable[OF initial[simplified ‹e = ev a›]]
        Aftertick_def T_After ‹e = ev a› hyp prems initial
      show ‹reachable_tick P r› by auto
    qed
  qed
qed



subsubsection ‹Properties›

corollary reachable_tick_set_is_mem_Collect_reachable_tick :
  ‹ℛ✓ P = {a. reachable_tick P a}›
  by (auto simp add: reachable_tick_set_def reachable_processes_is
      reachable_tick_iff_in_initials_Aftertrace_for_some_tickFree_T)  

corollary ticks_of_is_reachable_tick_set : ‹✓s(P) = ℛ✓ P›
  by (simp add: reachable_tick_set_is_mem_Collect_reachable_tick
      set_eq_iff ticks_of_iff_reachable_tick)

lemma ticks_of_reachable_processes_subset : ‹Q ∈ ℛproc P ⟹ ✓s(Q) ⊆ ✓s(P)›
  by (induct rule: reachable_processes.induct)
    (simp_all add: subset_iff ticks_of_iff_reachable_tick reachable_tick_after_reachable)

corollary ticks_of_antecedent_processes_superset : ‹Q ∈ 𝒜proc P ⟹ ✓s(P) ⊆ ✓s(Q)›
  by (simp add: antecedent_processes_iff_rev_reachable_processes
      ticks_of_reachable_processes_subset)

lemma ticks_of_is_Union_nth_initials: ‹✓s(P) = (⋃n. {r. ✓(r) ∈ P⇗n⇖})›
  by (auto simp add: nth_initials_is ticks_of_iff_reachable_tick
      reachable_tick_iff_in_initials_Aftertrace_for_some_tickFree_T)+






subsection ‹Characterizations for Deadlock Freeness› 

text ‹Remember that we have characterized term‹deadlock_free P› with an equality involving
      const‹Aftertick›: @{thm [show_question_marks=false] deadlock_free_Aftertick_characterization}.
      This can of course be derived in a characterization involving const‹Aftertrace›.›

lemma deadlock_free_Aftertrace_characterization:
  ‹deadlock_free P ⟷ (∀t ∈ 𝒯 P. range ev ∉ ℛa P t ∧ (t ≠ [] ⟶ deadlock_free (P after𝒯 t)))›
proof (intro iffI)
  show ‹deadlock_free P ⟹ ∀t∈𝒯 P. range ev ∉ ℛa P t ∧ (t ≠ [] ⟶ deadlock_free (P after𝒯 t))›
  proof (intro ballI)
    show ‹deadlock_free P ⟹ t ∈ 𝒯 P ⟹ range ev ∉ ℛa P t ∧ (t ≠ [] ⟶ deadlock_free (P after𝒯 t))› for t
    proof (induct t rule: rev_induct)
      case Nil
      thus ?case
        by (subst (asm) deadlock_free_Aftertick_characterization)
          (simp add: Refusals_after_def Nil.prems(1) Refusals_iff)
    next
      case (snoc e t)
      thus ?case
        by (simp add: Refusals_after_def Aftertrace_snoc)
          (metis Aftertrace.simps(1) Aftertrace_snoc DF_FD_Aftertick F_imp_R_Aftertrace T_F_spec
            deadlock_free_Aftertick_characterization deadlock_free_def 
            deadlock_free_implies_non_terminating initials_Aftertrace is_processT3)
    qed
  qed
  show ‹∀t∈𝒯 P. range ev ∉ ℛa P t ∧ (t ≠ [] ⟶ deadlock_free (P after𝒯 t)) ⟹ deadlock_free P›
    by (subst deadlock_free_Aftertick_characterization)
      (metis Aftertrace.simps Nil_elem_T Refusals_after_def
        Refusals_iff list.distinct(1) mem_Collect_eq initials_def)
qed   


lemma deadlock_freeSKIPS_Aftertrace_characterization: 
  ‹deadlock_freeSKIPS P ⟷
   (∀t ∈ 𝒯 P. tF t ⟶ UNIV ∉ ℛa P t ∧ (t ≠ [] ⟶ deadlock_freeSKIPS (P after𝒯 t)))›
  by (auto simp add: deadlock_freeSKIPS_is_right F_Aftertrace_eq T_Aftertrace_eq Refusals_after_def)


text ‹Actually, with @{const [source] Aftertrace}, we can obtain much more powerful results.
      This will be developed later.›



subsection ‹Continuity›

lemma Aftertrace_cont :
  ‹⟦∀a. ev a ∈ set t ⟶ cont (λP. Ψ P a);
    ∀r. ✓(r) ∈ set t ⟶ cont (λP. Ω P r); cont f⟧ ⟹
   cont (λx. f x after𝒯 t)›
proof (induct t arbitrary: f)
  case Nil thus ?case by simp
next
  case (Cons e s)
  show ?case by (cases e; simp, rule Cons.hyps) (simp_all add: Cons.prems)
qed



end

(*<*)
end
  (*>*)