Theory Operational_Semantics_Laws

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff.
 *
 * This file       : Common work for operational semantics
 *
 * 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 ‹ Generic Operational Semantics as a Locale›

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


paragraph ‹Some Properties of Monotony›

lemma FD_iff_eq_Ndet: ‹P ⊑FD Q ⟷ P = P ⊓ Q›
  by (auto simp add: Process_eq_spec failure_divergence_refine_def failure_refine_def
      divergence_refine_def F_Ndet D_Ndet)

lemma non_BOT_mono_Det_F :
  ‹P = ⊥ ∨ P' ≠ ⊥ ⟹ Q = ⊥ ∨ Q' ≠ ⊥ ⟹ P ⊑F P' ⟹ Q ⊑F Q' ⟹ P □ Q ⊑F P' □ Q'›
  using F_subset_imp_T_subset by (simp add: failure_refine_def F_Det BOT_iff_Nil_D) blast

lemma non_BOT_mono_Det_left_F  : ‹P = ⊥ ∨ P' ≠ ⊥ ∨ Q = ⊥ ⟹ P ⊑F P' ⟹ P □ Q ⊑F P' □ Q ›
  and non_BOT_mono_Det_right_F : ‹Q = ⊥ ∨ Q' ≠ ⊥ ∨ P = ⊥ ⟹ Q ⊑F Q' ⟹ P □ Q ⊑F P  □ Q'›
  by (metis Det_is_BOT_iff idem_F non_BOT_mono_Det_F)+

lemma non_BOT_mono_Sliding_F :
  ‹P = ⊥ ∨ P' ≠ ⊥ ∨ Q = ⊥ ⟹ P ⊑F P' ⟹ Q ⊑F Q' ⟹ P ⊳ Q ⊑F P' ⊳ Q'›
  unfolding Sliding_def by (metis Ndet_is_BOT_iff idem_F mono_Ndet_F non_BOT_mono_Det_F)



section ‹Definition›

locale OpSemTransitions = AfterExt Ψ Ω
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick› 
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    ― ‹Just declaring the types typ‹'a› and typ‹'r›.› +
  fixes τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50)
  assumes τ_trans_NdetL: ‹P ⊓ Q ↝τ P›
    and τ_trans_transitivity: ‹P ↝τ Q ⟹ Q ↝τ R ⟹ P ↝τ R›
    and τ_trans_anti_mono_initials: ‹P ↝τ Q ⟹ initials Q ⊆ initials P›
    and τ_trans_mono_Aftertick: ‹e ∈ initials Q ⟹ P ↝τ Q ⟹ P after✓ e ↝τ Q after✓ e›

begin

text ‹This locale needs to be instantiated with:
      ▪ a function @{term [show_types = true] Ψ} that is a placeholder for the value
        of term‹P after e› when term‹ev e ∉ initials P›
      ▪ a function @{term [show_types = true] Ω} that is a placeholder for the value
        of term‹P after✓ ✓(r)›
      ▪ a binary relation @{term [show_types] ‹(↝τ)›} which:
        ▪ is compatible with const‹Ndet›
        ▪ is transitive
        ▪ makes const‹initials› anti-monotonic
        ▪ makes @{const [source] Aftertick} monotonic.›

text ‹From the ‹τ› transition term‹P ↝τ Q› we derive the event transition as follows:›

abbreviation ev_trans :: ‹[('a, 'r) processptick, 'a, ('a, 'r) processptick] ⇒ bool› (‹_ ↝⇘_⇙ _› [50, 3, 51] 50)
  where ‹P ↝⇘e⇙ Q ≡ ev e ∈ P0 ∧ P after✓ ev e ↝τ Q›

abbreviation tick_trans :: ‹[('a, 'r) processptick, 'r, ('a, 'r) processptick] ⇒ bool› (‹_ ↝✓⇘_⇙ _› [50, 3, 51] 50)
  where ‹P ↝✓⇘r⇙ Q ≡ ✓(r) ∈ P0 ∧ P after✓ ✓(r) ↝τ Q›

lemma ev_trans_is: ‹P ↝⇘e⇙ Q ⟷ ev e ∈ initials P ∧ P after e ↝τ Q›
  by (simp add: Aftertick_def)

lemma tick_trans_is: ‹P ↝✓⇘r⇙ Q ⟷ ✓(r) ∈ P0 ∧ Ω P r ↝τ Q›
  by (simp add: Aftertick_def)

lemma reverse_event_trans_is:
  ‹e ∈ P0 ∧ P after✓ e ↝τ Q ⟷ (case e of ✓(r) ⇒ P ↝✓⇘r⇙ Q | ev x ⇒ P ↝⇘x⇙ Q)›
  by (simp split: eventptick.split)



text ‹From idempotence, commutativity and term‹⊥› absorbency of term‹(⊓)›, 
      we get the following free of charge.›

lemma τ_trans_eq: ‹P ↝τ P›
  and τ_trans_NdetR: ‹P ⊓ Q ↝τ Q›
  and BOT_τ_trans_anything: ‹⊥ ↝τ P›
    apply (metis Ndet_id τ_trans_NdetL)
   apply (metis Ndet_commute τ_trans_NdetL)
  by (metis Ndet_BOT τ_trans_NdetL)

lemma BOT_ev_trans_anything: ‹⊥ ↝⇘e⇙ P›
  and BOT_tick_trans: ‹⊥ ↝✓⇘r⇙ Ω ⊥ r›
  by (simp_all add: Aftertick_BOT τ_trans_eq BOT_τ_trans_anything)



text ‹As immediate consequences of the axioms, we prove that event transitions 
      absorb ‹τ› transitions on right and on left.›

lemma   ev_trans_τ_trans: ‹P ↝⇘e⇙ P' ⟹ P' ↝τ P'' ⟹ P ↝⇘e⇙ P''›
  and tick_trans_τ_trans: ‹P ↝✓⇘r⇙ P' ⟹ P' ↝τ P'' ⟹ P ↝✓⇘r⇙ P''›
  by (meson τ_trans_transitivity)+

lemma   τ_trans_ev_trans: ‹P ↝τ P' ⟹ P' ↝⇘e⇙ P'' ⟹ P ↝⇘e⇙ P''›
  and τ_trans_tick_trans: ‹P ↝τ P' ⟹ P' ↝✓⇘r⇙ P'' ⟹ P ↝✓⇘r⇙ P''›
  using τ_trans_mono_Aftertick τ_trans_transitivity τ_trans_anti_mono_initials by blast+



text ‹We can also add these result which will be useful later.›

lemma initial_tick_imp_τ_trans_SKIP: ‹P ↝τ SKIP r› if ‹✓(r) ∈ P0›
proof -
  from that have ‹P ⊑FD SKIP r› by (simp add: initial_tick_iff_FD_SKIP)
  with FD_iff_eq_Ndet have ‹P = P ⊓ SKIP r› ..
  thus ‹P ↝τ SKIP r› by (metis τ_trans_NdetR)
qed

lemma exists_tick_trans_is_initial_tick: ‹(∃P'. P ↝✓⇘r⇙ P') ⟷ ✓(r) ∈ P0›
  using τ_trans_eq by blast



text ‹There is also a major property we can already prove.›

lemma τ_trans_imp_leT : ‹P ↝τ Q ⟹ P ⊑T Q›
proof (unfold trace_refine_def, rule subsetI)
  show ‹P ↝τ Q ⟹ s ∈ 𝒯 Q ⟹ s ∈ 𝒯 P› for s
  proof (induct s arbitrary: P Q)
    show ‹⋀P. [] ∈ 𝒯 P› by simp
  next
    fix e s P Q
    assume   hyp : ‹P ↝τ Q ⟹ s ∈ 𝒯 Q ⟹ s ∈ 𝒯 P› for P Q
    assume prems : ‹P ↝τ Q› ‹e # s ∈ 𝒯 Q›
    from prems(2)[THEN initials_memI] have ‹e ∈ Q0› .
    show ‹e # s ∈ 𝒯 P›
    proof (cases e)
      fix r assume ‹e = ✓(r)›
      hence ‹s = []› by (metis append_Cons append_Nil append_T_imp_tickFree non_tickFree_tick prems(2))
      with ‹e = ✓(r)› ‹P ↝τ Q›[THEN τ_trans_anti_mono_initials] ‹e # s ∈ 𝒯 Q›
      show ‹e # s ∈ 𝒯 P› by (simp add: initials_def subset_iff)
    next
      fix x
      assume ‹e = ev x›
      from ‹e ∈ Q0› prems(2) have ‹s ∈ 𝒯 (Q after✓ e)› 
        by (simp add: ‹e = ev x› T_Aftertick)
      from τ_trans_mono_Aftertick[OF ‹e ∈ Q0› ‹P ↝τ Q›]
      have ‹P after✓ e ↝τ Q after✓ e› .
      from hyp[OF this ‹s ∈ 𝒯 (Q after✓ e)›] have ‹s ∈ 𝒯 (P after✓ e)› .
      with ‹e ∈ Q0›[THEN ‹P ↝τ Q›[THEN τ_trans_anti_mono_initials, THEN set_mp]]
      show ‹e # s ∈ 𝒯 P› by (simp add: T_Aftertick ‹e = ev x›)
    qed
  qed
qed



text ‹We can now define the concept of transition with a trace 
      and demonstrate the first properties.›

inductive trace_trans :: ‹('a, 'r) processptick ⇒ ('a, 'r) traceptick ⇒ ('a, 'r) processptick ⇒ bool›
  (‹_ ↝*_ _› [50, 3, 51] 50)
  where    trace_τ_trans : ‹P ↝τ P' ⟹ P ↝* [] P'›
  |     trace_tick_trans : ‹P ↝✓⇘r⇙ P' ⟹ P ↝* [✓(r)] P'›
  |  trace_Cons_ev_trans : ‹P ↝⇘e⇙  P' ⟹ P' ↝* s P'' ⟹ P ↝* (ev e) # s P''›

lemma trace_trans_τ_trans: ‹P ↝*s P' ⟹ P' ↝τ P'' ⟹ P ↝*s P''›
  apply (induct rule: trace_trans.induct)
  using τ_trans_transitivity trace_τ_trans apply blast
  using τ_trans_transitivity trace_tick_trans apply blast
  using trace_Cons_ev_trans by blast

lemma τ_trans_trace_trans:  ‹P ↝τ P' ⟹ P' ↝*s P'' ⟹ P ↝*s P''›
  apply (rotate_tac, induct rule: trace_trans.induct)
  using τ_trans_transitivity trace_τ_trans apply blast
  using τ_trans_tick_trans trace_trans.simps apply blast
  using τ_trans_ev_trans trace_Cons_ev_trans by blast


lemma BOT_trace_trans_tickFree_anything : ‹tickFree s ⟹ ⊥ ↝*s P›
proof (induct s arbitrary: P)
  show ‹⋀P. tickFree [] ⟹ ⊥ ↝*[] P›
    by (simp add: BOT_τ_trans_anything trace_τ_trans)
next
  fix e s P
  assume prem: ‹tickFree (e # s)› and hyp: ‹tickFree s ⟹ ⊥ ↝*s P› for P
  have * : ‹tickFree s› using prem by auto
  obtain a where ‹e = ev a› by (meson is_ev_def prem tickFree_Cons_iff)
  thus ‹⊥ ↝*e # s P›
    by simp (rule trace_Cons_ev_trans[OF _ hyp];
        simp add: * Aftertick_BOT BOT_τ_trans_anything)
qed



section ‹Consequences of term‹P ↝*s Q› on term‹ℱ›, term‹𝒯› and term‹𝒟››

lemma trace_trans_imp_F_if_τ_trans_imp_leF:
  ‹P ↝*s Q ⟹ X ∈ ℛ Q ⟹ (s, X) ∈ ℱ P›
  if ‹∀P Q. P ↝τ Q ⟶ P ⊑F Q›
proof (induct rule: trace_trans.induct)
  show ‹P ↝τ Q ⟹ X ∈ ℛ Q ⟹ ([], X) ∈ ℱ P› for P Q
    by (meson failure_refine_def in_mono Refusals_iff that)
next
  show ‹P ↝✓⇘r⇙ Q ⟹ X ∈ ℛ Q ⟹ ([✓(r)], X) ∈ ℱ P› for P Q r
    by (metis append_Nil mem_Collect_eq initials_def tick_T_F)
next
  fix P e Q s Q'
  assume * : ‹P ↝⇘e⇙ Q› ‹X ∈ ℛ Q' ⟹ (s, X) ∈ ℱ Q› ‹X ∈ ℛ Q'›
  have ‹P after✓ ev e ⊑F Q› using *(1) that by blast
  hence ‹(s, X) ∈ ℱ (P after✓ ev e)› by (simp add: failure_refine_def subsetD *(2, 3))
  thus ‹(ev e # s, X) ∈ ℱ P› by (simp add: F_Aftertick *(1))
qed


lemma trace_trans_imp_T: ‹P ↝*s Q ⟹ s ∈ 𝒯 P› 
proof (induct rule: trace_trans.induct)
  show ‹P ↝τ Q ⟹ [] ∈ 𝒯 P› for P Q by simp
next
  show ‹P ↝✓⇘r⇙ Q ⟹ [✓(r)] ∈ 𝒯 P› for P Q r
    by (simp add: initials_def)
next
  fix P e Q s Q'
  assume * : ‹P ↝⇘e⇙ Q› ‹s ∈ 𝒯 Q›
  have ‹P after✓ ev e ⊑T Q› using *(1) τ_trans_imp_leT by blast
  hence ‹s ∈ 𝒯 (P after✓ ev e)› by (simp add: *(2) subsetD trace_refine_def)
  with *(1) list.collapse show ‹ev e # s ∈ 𝒯 P› 
    by (force simp add: T_Aftertick initials_def)
qed


(* see if this hypothesis can be in the locale assumptions *)
(* the previous version was with (∀P Q. P ↝τ Q ⟶ P ⊑D Q),
   which is a stronger assumption *)
lemma tickFree_trace_trans_BOT_imp_D_if_τ_trans_BOT_imp_eq_BOT_weak:
  ‹tickFree s ⟹ P ↝*s ⊥ ⟹ s ∈ 𝒟 P› 
  if ‹∀P. P ↝τ ⊥ ⟶ P = ⊥›
proof (induct s arbitrary: P)
  show ‹P ↝*[] ⊥ ⟹ [] ∈ 𝒟 P› for P
    apply (erule trace_trans.cases)
    using BOT_iff_Nil_D that by blast+
next
  fix e s P
  assume prems : ‹tickFree (e # s)› ‹P ↝*e # s ⊥› 
  assume hyp: ‹tickFree s ⟹ P ↝*s ⊥ ⟹ s ∈ 𝒟 P› for P
  from prems(1) have ‹tickFree s› by simp
  from prems(2) have ‹P after✓ e ↝*s ⊥›
    by (cases rule: trace_trans.cases)
      (auto simp add:  trace_τ_trans intro: τ_trans_trace_trans)
  show ‹e # s ∈ 𝒟 P›
    apply (rule trace_trans.cases[OF prems(2)])
    using hyp[OF ‹tickFree s› ‹P after✓ e ↝*s ⊥›] prems(1)
    by (simp_all add: D_Aftertick)
qed



section ‹Characterizations for term‹P ↝*s Q››

lemma trace_trans_iff :
  ‹P ↝* [] Q ⟷ P ↝τ Q›
  ‹P ↝* [✓(r)] Q ⟷ P ↝✓⇘r⇙ Q›
  ‹P ↝* (ev e) # s Q' ⟷ (∃Q. P ↝⇘e⇙ Q ∧ Q ↝* s Q')›
  ‹(P ↝* s @ [f] Q') ⟷ 
   tickFree s ∧ (∃Q. P ↝*s Q ∧ (case f of ✓(r) ⇒ Q ↝✓⇘r⇙ Q' | ev x ⇒ Q ↝⇘x⇙ Q'))›
  ‹front_tickFree (s @ t) ⟹ (P ↝*s @ t Q') ⟷ (∃Q. P ↝*s Q ∧ Q ↝*t Q')›
proof -
  show f1 : ‹⋀P Q. P ↝* [] Q ⟷ P ↝τ Q›
    and f2 : ‹⋀P Q. P ↝* [✓(r)] Q ⟷ P ↝✓⇘r⇙  Q›
    and f3 : ‹⋀P Q' e. P ↝* (ev e) # s Q' ⟷ (∃Q. P ↝⇘e⇙ Q ∧ Q ↝* s Q')›
    by ((subst trace_trans.simps, auto)[1])+

  show f4 : ‹(P ↝* s @ [f] Q') ⟷ 
             tickFree s ∧ (∃Q. P ↝*s Q ∧ (case f of ✓(r) ⇒ Q ↝✓⇘r⇙ Q' | ev x ⇒ Q ↝⇘x⇙ Q'))› for s f P Q'
  proof safe
    from append_T_imp_tickFree trace_trans_imp_T
    show ‹P ↝*s @ [f] Q' ⟹ tickFree s› by blast
  next
    show ‹P ↝*s @ [f] Q' ⟹ ∃Q. P ↝*s Q ∧ (case f of ev x ⇒ Q ↝⇘x⇙ Q' | ✓(r) ⇒ Q ↝✓⇘r⇙ Q')›
    proof (induct s arbitrary: P)
      case Nil
      thus ?case 
        apply (subst (asm) trace_trans.simps, cases f; simp)
        using τ_trans_eq τ_trans_transitivity f1 by blast+
    next
      case (Cons e s)
      from Cons.prems have * : ‹e ∈ initials P ∧ P after✓ e ↝*s @ [f] Q'›
        by (subst (asm) trace_trans.simps)
          (auto simp add:  intro: τ_trans_trace_trans)
      with Cons.hyps obtain Q
        where ** : ‹P after✓ e ↝*s Q› 
          ‹(case f of ev x ⇒ Q ↝⇘x⇙ Q' | ✓(r) ⇒ Q ↝✓⇘r⇙ Q')› by blast
      have ‹P ↝*e # s Q›
      proof (cases e)
        fix e'
        assume ‹e = ev e'›
        thus ‹P ↝*e # s Q›
          apply simp
          by (rule trace_Cons_ev_trans[OF _ **(1)]) (use * τ_trans_eq in blast)
      next
        from Cons.prems have ‹e = ✓(r) ⟹ s = []› for r by (subst (asm) trace_trans.simps) auto
        thus ‹e = ✓(r) ⟹ P ↝*e # s Q› for r using * **(1) f1 f2 trace_tick_trans by auto
      qed
      with "**"(2) show ‹∃Q. P ↝* e # s Q ∧ (case f of ev x ⇒ Q ↝⇘x⇙ Q' | ✓(r) ⇒ Q ↝✓⇘r⇙ Q')› by blast
    qed
  next
    show ‹tickFree s ⟹ P ↝*s Q ⟹ (case f of ev x ⇒ Q ↝⇘x⇙ Q' | ✓(r) ⇒ Q ↝✓⇘r⇙ Q')
          ⟹ P ↝*s @ [f] Q'› for Q
    proof (induct s arbitrary: P Q)
      show ‹tickFree [] ⟹ P ↝*[] Q ⟹
            (case f of ev x ⇒ Q ↝⇘x⇙ Q' | ✓(r) ⇒ Q ↝✓⇘r⇙ Q') ⟹ P ↝*[] @ [f] Q'› for P Q
        apply (cases f; simp add: f1 f2)
         apply (meson τ_trans_eq τ_trans_ev_trans trace_Cons_ev_trans trace_τ_trans)
        using τ_trans_tick_trans trace_tick_trans by blast
    next
      case (Cons e s)
      from Cons.prems(2) have * : ‹e ∈ initials P ∧ P after✓ e ↝*s Q›
        by (subst (asm) trace_trans.simps)
          (auto simp add: f1 intro: τ_trans_trace_trans)
      show ?case
      proof (cases e)
        fix e'
        assume ‹e = ev e'›
        thus ‹P ↝*(e # s) @ [f] Q'› 
          by (cases f; simp)
            (metis (no_types, lifting) "*" Cons.hyps Cons.prems(1, 3) 
              τ_trans_eq tickFree_Cons_iff trace_trans.simps)+
      next
        show ‹e = ✓(r) ⟹ P ↝*(e # s) @ [f] Q'› for r using Cons.prems(1) by auto
      qed
    qed
  qed

  show ‹front_tickFree (s @ t) ⟹ P ↝*s @ t Q' ⟷ (∃Q. P ↝*s Q ∧ Q ↝*t Q')›
  proof (induct t arbitrary: Q' rule: rev_induct)
    show ‹P ↝*s @ [] Q' ⟷ (∃Q. P ↝*s Q ∧ Q ↝*[] Q')› for Q'
      by (metis τ_trans_eq append.right_neutral trace_trans_τ_trans f1)
  next
    case (snoc e t)
    from snoc.prems have $ : ‹tickFree s› ‹tickFree t› 
      by (simp_all add: front_tickFree_append_iff)
    show ‹P ↝*s @ t @ [e] Q' ⟷ (∃Q. P ↝*s Q ∧ Q ↝*t @ [e] Q')›
    proof (intro iffI)
      assume assm : ‹P ↝*s @ t @ [e] Q'›
      from f4[of P ‹s @ t› e Q', simplified] assm "$" obtain Q
        where * : ‹P ↝*s @ t Q› ‹case e of ev x ⇒ Q ↝⇘x⇙ Q' | ✓(r) ⇒ Q ↝✓⇘r⇙ Q'› by blast
      obtain R where ** : ‹P ↝*s R› ‹R ↝*t Q›
        by (metis "*"(1) append.assoc front_tickFree_dw_closed snoc.hyps snoc.prems)
      show ‹∃Q. P ↝*s Q ∧ Q ↝*t @ [e] Q'›
      proof (intro exI conjI)
        show ‹P ↝*s R› by (fact "**"(1))
      next
        from "*"(2) "**"(2) show ‹R ↝*t @ [e] Q'› by (simp add: f4 "$"(2)) blast
      qed
    next
      assume ‹∃Q. P ↝*s Q ∧ Q ↝*t @ [e] Q'›
      then obtain Q where * : ‹P ↝*s Q› ‹Q ↝*t @ [e] Q'› by blast
      from f4[of Q t e Q', simplified this(2)]
      obtain R where ‹Q ↝*t R› ‹case e of ev x ⇒ R ↝⇘x⇙ Q' | ✓(r) ⇒ R ↝✓⇘r⇙ Q'› by blast
      with "*"(1) show ‹P ↝*s @ t @ [e] Q'›
        by (simp add: f4[of P ‹s @ t› e Q', simplified] "$", cases e; simp)
          (metis append.assoc front_tickFree_dw_closed snoc.hyps snoc.prems)+
    qed
  qed
qed



section ‹Finally: term‹P ↝*s Q› is term‹P after𝒯 s ↝τ Q››

theorem trace_trans_iff_T_and_Aftertrace_τ_trans : 
  ‹(P ↝*s Q) ⟷ s ∈ 𝒯 P ∧ P after𝒯 s ↝τ Q›
proof -
  have ‹s ∈ 𝒯 P ⟹ (P ↝*s Q) ⟷ P after𝒯 s ↝τ Q›
    ―‹This is a trick to reuse the proof of this less powerful version
     (@{thm [source] trace_trans_imp_T} was not proven at the time‹…›).›
  proof (intro iffI)
    show ‹P ↝*s Q ⟹ s ∈ 𝒯 P ⟹ P after𝒯 s ↝τ Q›
    proof (induct s arbitrary: P Q)
      show ‹⋀P Q. P ↝*[] Q ⟹ [] ∈ 𝒯 P ⟹ P after𝒯 [] ↝τ Q›
        using trace_trans.cases by auto
    next
      show ‹(⋀P Q. P ↝*s Q ⟹ s ∈ 𝒯 P ⟹ P after𝒯 s ↝τ Q) ⟹ 
            P ↝*e # s Q ⟹ e # s ∈ 𝒯 P ⟹ P after𝒯 (e # s) ↝τ Q› for s e P Q
        apply (cases e; simp)
        by (meson τ_trans_trace_trans trace_trans_iff(3) trace_trans_imp_T)
          (metis Aftertrace.simps(1) T_imp_front_tickFree front_tickFree_Cons_iff
            non_tickFree_tick tickFree_Cons_iff tickFree_Nil trace_trans_iff(2))
    qed
  next
    show ‹P after𝒯 s ↝τ Q ⟹ s ∈ 𝒯 P ⟹ P ↝*s Q›
    proof (induct arbitrary: P Q rule: Aftertrace.induct)
      show ‹⋀P Q. P after𝒯 [] ↝τ Q ⟹ [] ∈ 𝒯 P ⟹ P ↝*[] Q›
        by (simp add: trace_τ_trans)
    next
      fix e and s :: ‹('a, 'r) traceptick› and Q P
      assume   hyp : ‹P after𝒯 s ↝τ Q ⟹ s ∈ 𝒯 P ⟹ P ↝*s Q› for P Q
      assume prems : ‹P after𝒯 (e # s) ↝τ Q› ‹e # s ∈ 𝒯 P›
      have * : ‹e ∈ initials P ∧ s ∈ 𝒯 (P after✓ e)›
        by (metis Aftertrace.simps(1, 2) initials_memI 
            T_Aftertrace append_Cons append_Nil prems(2))
      show ‹P ↝*e # s Q›
      proof (cases e)
        fix e'
        assume ** : ‹e = ev e'›
        from * ** have ‹P ↝⇘e'⇙ P after✓ (ev e')› by (simp add: τ_trans_eq)
        thus ‹P ↝*e # s Q›
          by (subst **, rule trace_Cons_ev_trans[OF _ hyp[OF prems(1)[simplified] 
                  *[THEN conjunct2], simplified **]])
      next
        have ‹e = ✓(r) ⟹ s = []› for r
          by (metis T_imp_front_tickFree eventptick.disc(2) front_tickFree_Cons_iff prems(2))
        with "*" prems(1) trace_tick_trans
        show ‹e = ✓(r) ⟹ P ↝*e # s Q› for r by auto
      qed
    qed
  qed
  with trace_trans_imp_T show ‹(P ↝*s Q) ⟷ s ∈ 𝒯 P ∧ P after𝒯 s ↝τ Q› by blast
qed



text ‹As corollaries we obtain the reciprocal results of 

      @{thm trace_trans_imp_F_if_τ_trans_imp_leF
            trace_trans_imp_T
            tickFree_trace_trans_BOT_imp_D_if_τ_trans_BOT_imp_eq_BOT_weak}›

lemma tickFree_F_imp_exists_trace_trans:
  ‹tickFree s ⟹ (s, X) ∈ ℱ P ⟹ ∃Q. (P ↝*s Q) ∧ X ∈ ℛ Q›
  by (meson F_T F_imp_R_Aftertrace trace_trans_iff_T_and_Aftertrace_τ_trans τ_trans_eq)

lemma T_imp_exists_trace_trans: ‹s ∈ 𝒯 P ⟹ ∃Q. P ↝*s Q›
  using trace_trans_iff_T_and_Aftertrace_τ_trans τ_trans_eq by blast

lemma tickFree_D_imp_trace_trans_BOT: ‹tickFree s ⟹ s ∈ 𝒟 P ⟹ P ↝*s ⊥›
  by (simp add: D_imp_Aftertrace_is_BOT D_T τ_trans_eq
      trace_trans_iff_T_and_Aftertrace_τ_trans)


text ‹And therefore, we obtain equivalences.›

lemma F_trace_trans_reality_check_weak: 
  ‹∀P Q. P ↝τ Q ⟶ P ⊑F Q ⟹ tickFree s ⟹ 
   (s, X) ∈ ℱ P ⟷ (∃Q. (P ↝*s Q) ∧ X ∈ ℛ Q)›
  using tickFree_F_imp_exists_trace_trans trace_trans_imp_F_if_τ_trans_imp_leF by blast

lemma T_trace_trans_reality_check: ‹s ∈ 𝒯 P ⟷ (∃Q. P ↝*s Q)›
  using T_imp_exists_trace_trans trace_trans_imp_T by blast

lemma D_trace_trans_reality_check_weak:
  ‹∀P. P ↝τ ⊥ ⟶ P = ⊥ ⟹ tickFree s ⟹ s ∈ 𝒟 P ⟷ P ↝*s ⊥›
  using tickFree_D_imp_trace_trans_BOT
    tickFree_trace_trans_BOT_imp_D_if_τ_trans_BOT_imp_eq_BOT_weak by blast




text ‹When we have more information on term‹P ↝τ Q›, we obtain:›

lemma STOP_trace_trans_iff: ‹STOP ↝*s P ⟷ s = [] ∧ P = STOP›
  using STOP_T_iff τ_trans_imp_leT 
  by (subst trace_trans.simps) (auto simp add: τ_trans_eq) 


lemma Ω_SKIP_is_STOP_imp_τ_trans_imp_leF_imp_SKIP_trace_trans_iff: 
  ‹Ω (SKIP r) r = STOP ⟹ (⋀P Q. P ↝τ Q ⟹ P ⊑F Q) ⟹
   (SKIP r ↝*s P) ⟷ s = [] ∧ P = SKIP r ∨ s = [✓(r)] ∧ P = STOP›
  using SKIP_F_iff STOP_F_iff
  apply (subst trace_trans.simps)
  apply (auto simp add: Aftertick_SKIP τ_trans_eq)
  by fastforce blast+


lemma trace_trans_imp_initials_subset_initials_Aftertrace:
  ‹P ↝*s Q ⟹ initials Q ⊆ initials (P after𝒯 s)›
  using trace_trans_iff_T_and_Aftertrace_τ_trans 
    anti_mono_initials_T trace_trans_imp_T τ_trans_imp_leT by blast


lemma imp_trace_trans_imp_initial:
  ‹P ↝*(s @ e # t) Q ⟹ e ∈ initials (P after𝒯 s)›
  using initials_Aftertrace trace_trans_imp_T by blast



text ‹Under additional assumptions, we can show that the event
      transition and the trace transition are admissible.›

lemma ev_trans_adm_weak[simp]:
  assumes τ_trans_adm:
    ‹⋀u v. cont (u :: 'b :: cpo ⇒ ('a, 'r) processptick) ⟹ monofun v ⟹ adm(λx. u x ↝τ v x)›
    and Ψ_cont_hyp : ‹cont (λP. Ψ P e)›
    and cont_u: ‹cont (u :: 'b ⇒ ('a, 'r) processptick)› and monofun_v : ‹monofun v›
  shows ‹adm(λx. u x ↝⇘e⇙ (v x))›
  apply (intro adm_conj)
  by (fact initial_adm[OF cont_u])
    (rule τ_trans_adm[OF _ monofun_v], simp add: Ψ_cont_hyp cont_u)

lemma tick_trans_adm_weak[simp]:
  assumes τ_trans_adm:
    ‹⋀u v. cont (u :: 'b :: cpo ⇒ ('a, 'r) processptick) ⟹ monofun v ⟹ adm(λx. u x ↝τ v x)›
    and Ω_cont_hyp : ‹cont (λP. Ω P r)›
    and cont_u: ‹cont (u :: 'b ⇒ ('a, 'r) processptick)› and monofun_v : ‹monofun v›
  shows ‹adm(λx. u x ↝✓⇘r⇙ (v x))›
  apply (intro adm_conj)
  by (fact initial_adm[OF cont_u])
    (rule τ_trans_adm[OF _ monofun_v], simp add: Ω_cont_hyp cont_u)

lemma trace_trans_adm_weak[simp]:
  assumes τ_trans_adm: ‹⋀u v. cont (u :: 'b :: cpo ⇒ ('a, 'r) processptick) ⟹ monofun v ⟹ adm (λx. u x ↝τ v x)›
    and Aftertrace_cont_hyps: ‹∀x. ev x ∈ set s ⟶ cont (λP. Ψ P x)› ‹∀r. ✓(r) ∈ set s ⟶ cont (λP. Ω P r)›
    and cont_u: ‹cont (u :: 'b :: cpo ⇒ ('a, 'r) processptick)› and monofun_v: ‹monofun v›
  shows ‹adm (λx. u x ↝* s (v x))›
  apply (subst trace_trans_iff_T_and_Aftertrace_τ_trans)
  apply (intro adm_conj)
   apply (solves ‹simp add: adm_in_T cont_u›)
  by (rule τ_trans_adm[OF _ monofun_v], rule Aftertrace_cont; 
      simp add: Aftertrace_cont_hyps cont_u)



section ‹General Rules of Operational Semantics›

text ‹We can now derive some rules or the operational semantics that we are defining.›

(* maybe also write the rules for event_trans when it's consequence of τ_trans *)

(* assumes Ω_SKIP_is_STOP : ‹Ω SKIP = STOP› in a extension of the locale ?
   not really useful yet, we will just put Ω SKIP instead of STOP *)

lemma SKIP_trans_tick_Ω_SKIP: ‹SKIP r ↝✓⇘r⇙ Ω (SKIP r) r›
  by (simp add: Aftertick_SKIP τ_trans_eq)

lemmas SKIP_OpSem_rule = SKIP_trans_tick_Ω_SKIP

text ‹This is quite obvious, but we can get better.›

lemma initial_tick_imp_tick_trans_Ω_SKIP: ‹✓(r) ∈ P0 ⟹ P↝✓⇘r⇙ Ω (SKIP r) r›
  using SKIP_trans_tick_Ω_SKIP τ_trans_tick_trans
    initial_tick_imp_τ_trans_SKIP by blast

lemma tick_trans_imp_tick_trans_Ω_SKIP : ‹∃P'. P ↝✓⇘r⇙ P' ⟹ P↝✓⇘r⇙ Ω (SKIP r) r›
  using initial_tick_imp_tick_trans_Ω_SKIP by blast


(* lemma tick_trans_imp_BOT_L_or_STOP_R: ‹P ↝✓ Q ⟹ P = ⊥ ∨ Q = STOP›
  by (metis τ_trans_anti_mono_initials initials_Aftertick initials_empty_iff_STOP subset_empty)

lemma STOP_trace_trans_iff : ‹STOP ↝*s P ⟷ s = [] ∧ P = STOP›
  by (metis Aftertick_SKIP SKIP_neq_BOT SKIP_trans_tick empty_iff trace_trans.cases
            initials_STOP tick_trans_imp_BOT_L_or_STOP_R trace_trans_iff(1))

 *)


(* 

lemma tick_trans_iff : ‹P ↝✓ P' ⟷ P = ⊥ ∨ P ↝τ SKIP ∧ P' = STOP›
  by (metis Aftertick_BOT BOT_τ_trans_anything SKIP_trans_tick τ_trans_event_trans 
            initial_tick_imp_τ_trans_SKIP tick_trans_imp_BOT_L_or_STOP_R) *)


lemma SKIP_cant_ev_trans:   ‹¬ SKIP r ↝⇘e⇙ P›
  and STOP_cant_ev_trans:   ‹¬ STOP ↝⇘e⇙ P›
  and STOP_cant_tick_trans: ‹¬ STOP ↝✓⇘r⇙ P› by simp_all




lemma ev_trans_Mprefix: ‹e ∈ A ⟹ □a ∈ A → P a ↝⇘e⇙ (P e)›
  by (simp add: Aftertick_def After_Mprefix τ_trans_eq initials_Mprefix)

lemma ev_trans_Mndetprefix: ‹e ∈ A ⟹ ⊓a ∈ A → P a ↝⇘e⇙ (P e)›
  by (simp add: Aftertick_def After_Mndetprefix τ_trans_eq initials_Mndetprefix)

lemma ev_trans_prefix: ‹e → P ↝⇘e⇙ P›
  by (metis ev_trans_Mprefix insertI1 write0_def)

lemmas prefix_OpSem_rules = ev_trans_prefix ev_trans_Mprefix ev_trans_Mndetprefix



lemma τ_trans_GlobalNdet: ‹⊓a ∈ A. P a ↝τ P e› if ‹e ∈ A›
proof -
  have ‹⊓a ∈ A. P a = P e ⊓ (⊓a ∈ A. P a)›
    by (metis GlobalNdet_factorization_union GlobalNdet_unit
        empty_iff insertI1 insert_absorb insert_is_Un that)
  thus ‹⊓a ∈ A. P a ↝τ P e› by (metis τ_trans_NdetL)
qed

lemmas Ndet_OpSem_rules = τ_trans_NdetL τ_trans_NdetR τ_trans_GlobalNdet



lemma τ_trans_fix_point: ‹cont f ⟹ P = (μ X. f X) ⟹ P ↝τ f P›
  by (metis τ_trans_eq cont_process_rec)

lemmas fix_point_OpSem_rule = τ_trans_fix_point




lemma ev_trans_DetL: ‹P ↝⇘e⇙ P' ⟹ P □ Q ↝⇘e⇙ P'›
  by (metis Aftertick_Det_is_Aftertick_Ndet UnCI τ_trans_NdetL τ_trans_ev_trans initials_Det)

lemma ev_trans_DetR: ‹Q ↝⇘e⇙ Q' ⟹ P □ Q ↝⇘e⇙ Q'›
  by (metis Det_commute ev_trans_DetL)

lemma tick_trans_DetL: ‹P ↝✓⇘r⇙ P' ⟹ P □ Q ↝✓⇘r⇙ Ω (SKIP r) r›
  by (metis UnCI initials_Det initial_tick_imp_tick_trans_Ω_SKIP)

lemma tick_trans_DetR: ‹Q ↝✓⇘r⇙ Q' ⟹ P □ Q ↝✓⇘r⇙ Ω (SKIP r) r›
  by (metis Det_commute tick_trans_DetL)

lemma ev_trans_GlobalDet:
  ‹□a ∈ A. P a ↝⇘e⇙ Q› if ‹a ∈ A› and ‹P a ↝⇘e⇙ Q›
proof (cases ‹A = {a}›)
  show ‹A = {a} ⟹ □a ∈ A. P a ↝⇘e⇙ Q› by (simp add: ‹P a ↝⇘e⇙ Q›)
next
  assume ‹A ≠ {a}›
  with ‹a ∈ A› obtain A' where ‹a ∉ A'› ‹A = {a} ∪ A'›
    by (metis insert_is_Un mk_disjoint_insert)
  have ‹□a ∈ A. P a = P a □ GlobalDet A' P›
    by (simp add: ‹A = {a} ∪ A'› GlobalDet_distrib_unit_bis[OF ‹a ∉ A'›])
  also from ev_trans_DetL ‹P a ↝⇘e⇙ Q› have ‹… ↝⇘e⇙ Q› by blast
  finally show ‹□a ∈ A. P a ↝⇘e⇙ Q› .
qed

lemma tick_trans_GlobalDet:
  ‹□a ∈ A. P a ↝✓⇘r⇙ Ω (SKIP r) r› if ‹a ∈ A› and ‹P a ↝✓⇘r⇙ Q›
proof (cases ‹A = {a}›)
  show ‹A = {a} ⟹ □a ∈ A. P a ↝✓⇘r⇙ Ω (SKIP r) r›
    by (simp add: initial_tick_imp_tick_trans_Ω_SKIP ‹P a ↝✓⇘r⇙ Q›)
next
  assume ‹A ≠ {a}›
  with ‹a ∈ A› obtain A' where ‹a ∉ A'› ‹A = {a} ∪ A'›
    by (metis insert_is_Un mk_disjoint_insert)
  have ‹□a ∈ A. P a = P a □ GlobalDet A' P›
    by (simp add: ‹A = {a} ∪ A'› GlobalDet_distrib_unit_bis[OF ‹a ∉ A'›])
  also from tick_trans_DetL ‹P a ↝✓⇘r⇙ Q› have ‹… ↝✓⇘r⇙ Ω (SKIP r) r› by blast
  finally show ‹□a ∈ A. P a ↝✓⇘r⇙ Ω (SKIP r) r› .
qed



lemma ev_trans_SlidingL: ‹P ↝⇘e⇙ P' ⟹ P ⊳ Q ↝⇘e⇙ P'›
  by (simp add: Sliding_def)
    (meson τ_trans_NdetL τ_trans_ev_trans ev_trans_DetL)

lemma tick_trans_SlidingL: ‹P ↝✓⇘r⇙ P' ⟹ P ⊳ Q ↝✓⇘r⇙ Ω (SKIP r) r›
  by (metis UnCI initials_Sliding initial_tick_imp_tick_trans_Ω_SKIP)

lemma τ_trans_SlidingR: ‹P ⊳ Q ↝τ Q›
  by (simp add: Sliding_def τ_trans_NdetR)



(* a very good surprise *)
lemma τ_trans_SeqR: ‹P ; Q ↝τ Q'› if ‹P ↝✓⇘r⇙ P'› and ‹Q ↝τ Q'›
proof -
  from that(1) have ‹P ⊑FD SKIP r› by (simp add: initial_tick_iff_FD_SKIP)
  with FD_iff_eq_Ndet have ‹P = P ⊓ SKIP r› ..
  hence ‹P ; Q = (P ; Q) ⊓ (SKIP r ; Q)› by (metis Seq_distrib_Ndet_right)
  also have ‹… = (P ; Q) ⊓ Q› by simp
  also have ‹… ↝τ Q› by (simp add: τ_trans_NdetR)
  finally show ‹P ; Q ↝τ Q'› by (rule τ_trans_transitivity) (fact that(2))
qed

(* obvious now *)
lemma ‹✓(r) ∈ P0 ⟹ Q ↝⇘e⇙ Q' ⟹ P ; Q ↝⇘e⇙ Q'›
  using τ_trans_SeqR τ_trans_eq τ_trans_ev_trans by blast

(* we can't recover the rules for left side yet *)



lemma tick_trans_Hiding: ‹P ↝✓⇘r⇙ P' ⟹ P \ B ↝✓⇘r⇙ Ω (SKIP r) r›
  by (simp add: initial_tick_imp_tick_trans_Ω_SKIP initial_tick_imp_initial_tick_Hiding)


(* of course we can't recover τ_trans yet, and idem for inside and not inside rules*)



lemma τ_trans_SKIP_SyncL: ‹P ⟦S⟧ Q ↝τ SKIP r ⟦S⟧ Q› if ‹P ↝✓⇘r⇙ P'›
proof -
  from that have ‹P ⊑FD SKIP r› by (simp add: initial_tick_iff_FD_SKIP)
  with FD_iff_eq_Ndet have ‹P = P ⊓ SKIP r› ..
  hence ‹P ⟦S⟧ Q = (P ⟦S⟧ Q) ⊓ (SKIP r ⟦S⟧ Q)› by (metis Sync_distrib_Ndet_right)
  also have ‹… ↝τ (SKIP r ⟦S⟧ Q)› by (rule τ_trans_NdetR)
  finally show ‹P ⟦S⟧ Q ↝τ SKIP r ⟦S⟧ Q› .
qed

lemma τ_trans_SKIP_SyncR: ‹Q ↝✓⇘r⇙ Q' ⟹ P ⟦S⟧ Q ↝τ P ⟦S⟧ SKIP r›
  by (metis Sync_commute τ_trans_SKIP_SyncL)

lemma tick_trans_SKIP_Sync_SKIP: ‹SKIP r ⟦S⟧ SKIP r ↝✓⇘r⇙ Ω (SKIP r) r›
  by (simp add: SKIP_trans_tick_Ω_SKIP)

lemma ‹SKIP r ⟦S⟧ SKIP r ↝τ SKIP r›
  by (simp add: τ_trans_eq)



lemma tick_trans_InterruptL : ‹P ↝✓⇘r⇙ P' ⟹ P △ Q ↝✓⇘r⇙ Ω (SKIP r) r›
  and tick_trans_InterruptR : ‹Q ↝✓⇘r⇙ Q' ⟹ P △ Q ↝✓⇘r⇙ Ω (SKIP r) r›
  by (rule initial_tick_imp_tick_trans_Ω_SKIP, simp add: initials_Interrupt)+


lemma tick_trans_ThrowL : ‹P ↝✓⇘r⇙ P' ⟹ P Θ a ∈ A. Q a ↝✓⇘r⇙ Ω (SKIP r) r›
  by (rule initial_tick_imp_tick_trans_Ω_SKIP)
    (simp add: initials_Throw)

lemma ev_trans_ThrowR_inside:
  ‹e ∈ A ⟹ P ↝⇘e⇙ P' ⟹ P Θ a ∈ A. Q a ↝⇘e⇙ (Q e)›
  by (simp add: Aftertick_Throw initials_Throw BOT_τ_trans_anything τ_trans_eq)

end



section ‹Recovering other operational rules›

text ‹By adding a ‹τ›-transition hypothesis on each operator,
      we can recover the remaining operational rules.›

subsection ‹@{const [source] Det} Laws›

locale OpSemTransitionsDet = OpSemTransitions Ψ Ω ‹(↝τ)› 
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50) +
  assumes τ_trans_DetL : ‹P ↝τ P' ⟹ P □ Q ↝τ P' □ Q›
begin

lemma τ_trans_DetR : ‹Q ↝τ Q' ⟹ P □ Q ↝τ P □ Q'›
  by (metis Det_commute τ_trans_DetL)

lemmas Det_OpSem_rules = τ_trans_DetL τ_trans_DetR
  ev_trans_DetL ev_trans_DetR
  tick_trans_DetL tick_trans_DetR

(* discuss the fact that we don't have the exact rules from Roscoe's book here *)
end


subsection ‹@{const [source] Det} relaxed Laws›

―‹Introduced to recover some rules with term‹(⊑F)› refinement.›

locale OpSemTransitionsDetRelaxed = OpSemTransitions Ψ Ω ‹(↝τ)› 
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50) +
  assumes τ_trans_DetL : ‹P = ⊥ ∨ P' ≠ ⊥ ∨ Q = ⊥ ⟹ P ↝τ P' ⟹ P □ Q ↝τ P' □ Q›
begin

lemma τ_trans_DetR : ‹Q = ⊥ ∨ Q' ≠ ⊥ ∨ Q = ⊥ ⟹ Q ↝τ Q' ⟹ P □ Q ↝τ P □ Q'›
  by (metis Det_commute τ_trans_DetL)

lemmas Det_OpSem_rules = τ_trans_DetL τ_trans_DetR
  ev_trans_DetL ev_trans_DetR
  tick_trans_DetL tick_trans_DetR

(* discuss the fact that we don't have the exact rules from Roscoe's book here *)
end



subsection ‹@{const [source] Seq} Laws›

locale OpSemTransitionsSeq = OpSemTransitions Ψ Ω ‹(↝τ)› 
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50) +
  assumes τ_trans_SeqL : ‹P ↝τ P' ⟹ P ; Q ↝τ P' ; Q›
begin

lemma ev_trans_SeqL: ‹P ↝⇘e⇙ P' ⟹ P ; Q ↝⇘e⇙ P' ; Q›
  apply (cases ‹P = ⊥›, solves ‹simp add: BOT_ev_trans_anything›)
  apply (simp add: Aftertick_Seq initials_Seq image_iff disjoint_iff)
  by (meson τ_trans_NdetL τ_trans_SeqL τ_trans_transitivity ev_trans_is)

lemmas Seq_OpSem_rules = τ_trans_SeqL ev_trans_SeqL τ_trans_SeqR

end



subsection ‹@{const [source] Renaming} Laws›

text ‹We are used to it now:  we need to duplicate the locale in order
      to obtain the rules for the const‹Renaming› operator.›

locale OpSemTransitionsDuplicated = 
  OpSemTransitionsα: OpSemTransitions Ψα Ωα ‹(α↝τ)› +
  OpSemTransitionsβ: OpSemTransitions Ψβ Ωβ ‹(β↝τ)›
  for Ψα :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ωα :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_transα :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹α↝τ› 50)
    and Ψβ :: ‹[('b, 's) processptick, 'b] ⇒ ('b, 's) processptick›
    and Ωβ :: ‹[('b, 's) processptick, 's] ⇒ ('b, 's) processptick›
    and τ_transβ :: ‹[('b, 's) processptick, ('b, 's) processptick] ⇒ bool› (infixl ‹β↝τ› 50)
begin

notation OpSemTransitionsα.ev_trans   (‹_ α↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsα.tick_trans (‹_ α↝✓⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsβ.ev_trans   (‹_ β↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsβ.tick_trans (‹_ β↝✓⇘_⇙ _› [50, 3, 51] 50)

lemma tick_trans_Renaming: ‹P α↝✓⇘r⇙ P' ⟹ Renaming P f g β↝✓⇘g r⇙ (Ωβ (SKIP (g r)) (g r))›
  by (metis OpSemTransitionsβ.initial_tick_imp_tick_trans_Ω_SKIP
      Renaming_SKIP mono_Renaming_FD initial_tick_iff_FD_SKIP)

end

sublocale OpSemTransitionsDuplicated ⊆ AfterExtDuplicated .
    ―‹Recovering @{thm [source] AfterExtDuplicated.Aftertick_Renaming}
   (and @{thm [source] AfterDuplicated.After_Renaming})›


locale OpSemTransitionsRenaming =
  OpSemTransitionsDuplicated Ψα Ωα τ_transα Ψβ Ωβ τ_transβ
  for Ψα :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ωα :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_transα :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹α↝τ› 50)
    and Ψβ :: ‹[('b, 's) processptick, 'b] ⇒ ('b, 's) processptick›
    and Ωβ :: ‹[('b, 's) processptick, 's] ⇒ ('b, 's) processptick›
    and τ_transβ :: ‹[('b, 's) processptick, ('b, 's) processptick] ⇒ bool› (infixl ‹β↝τ› 50) +
  assumes τ_trans_Renaming : ‹P α↝τ P' ⟹ Renaming P f g β↝τ Renaming P' f g›
begin

lemma ev_trans_Renaming: ‹Renaming P f g β↝⇘b⇙ (Renaming P' f g)›
  if ‹f a = b› and ‹P α↝⇘a⇙ P'›
proof (cases ‹P = ⊥›)
  show ‹P = ⊥ ⟹ Renaming P f g β↝⇘b⇙ (Renaming P' f g)›
    by (simp add: Aftertick_Renaming)
      (simp add: OpSemTransitionsβ.BOT_τ_trans_anything
        OpSemTransitionsβ.BOT_ev_trans_anything)
next
  assume non_BOT: ‹P ≠ ⊥›
  from that have initial : ‹∃a. ev a ∈ initials P ∧ f a = b› by blast
  show ‹Renaming P f g β↝⇘b⇙ (Renaming P' f g)›
  proof (intro conjI)
    from initial show ‹ev b ∈ (Renaming P f g)0›
      by (force simp add: initials_Renaming image_iff) 
  next
    show ‹OpSemTransitionsβ.Aftertick (Renaming P f g) (ev b) β↝τ Renaming P' f g›
      apply (simp add: Aftertick_Renaming non_BOT initial)
      apply (rule OpSemTransitionsβ.τ_trans_transitivity
          [OF OpSemTransitionsβ.τ_trans_GlobalNdet[of a] τ_trans_Renaming])
       apply (solves ‹simp add: that›)
      using OpSemTransitionsα.ev_trans_is that(2) by blast
  qed
qed

lemmas Renaming_OpSem_rules = τ_trans_Renaming tick_trans_Renaming ev_trans_Renaming

end



subsection ‹@{const [source] Hiding} Laws›

locale OpSemTransitionsHiding = OpSemTransitions Ψ Ω ‹(↝τ)› 
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50) +
  assumes τ_trans_Hiding : ‹P ↝τ P' ⟹ P \ A ↝τ P' \ A›
begin

lemma τ_trans_Hiding_inside: ‹P \ A ↝τ P' \ A› if ‹e ∈ A› and ‹P ↝⇘e⇙ P'›
proof -
  have ‹P \ A ⊑FD P after✓ ev e \ A›
    by (simp add: Hiding_FD_Hiding_Aftertick_if_initial_inside that)
  with FD_iff_eq_Ndet have ‹P \ A = (P \ A) ⊓ (P after✓ ev e \ A)› ..
  moreover have ‹… ↝τ P after✓ ev e \ A› by (simp add: τ_trans_NdetR)
  moreover have ‹… ↝τ P' \ A› by (simp add: τ_trans_Hiding that(2))
  ultimately show ‹P \ A ↝τ P' \ A› by (metis τ_trans_transitivity)
qed


lemma ev_trans_Hiding_notin: ‹P \ A ↝⇘e⇙ P' \ A› if ‹e ∉ A› and ‹P ↝⇘e⇙ P'›
proof -
  note initial = initial_notin_imp_initial_Hiding[OF that(2)[THEN conjunct1] that(1)]
  have ‹(P \ A) after✓ ev e ⊑FD P after✓ ev e \ A›
    by (simp add: Aftertick_Hiding_FD_Hiding_Aftertick_if_initial_notin that)
  with FD_iff_eq_Ndet
  have ‹(P \ A) after✓ ev e = (P \ A) after✓ ev e ⊓ (P after✓ ev e \ A)› ..
  moreover have ‹… ↝τ P after✓ ev e \ A› by (simp add: τ_trans_NdetR)
  moreover have ‹… ↝τ P' \ A› by (simp add: τ_trans_Hiding that(2))
  ultimately show ‹P \ A ↝⇘e⇙ P' \ A› by (metis (no_types) τ_trans_transitivity initial)
qed

lemmas Hiding_OpSem_rules = τ_trans_Hiding tick_trans_Hiding
  ev_trans_Hiding_notin τ_trans_Hiding_inside

end



subsection ‹@{const [source] Sync} Laws›

locale OpSemTransitionsSync = OpSemTransitions Ψ Ω ‹(↝τ)› 
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50) +
  assumes τ_trans_SyncL : ‹P ↝τ P' ⟹ P ⟦S⟧ Q ↝τ P' ⟦S⟧ Q›
begin

lemma τ_trans_SyncR : ‹Q ↝τ Q' ⟹ P ⟦S⟧ Q ↝τ P ⟦S⟧ Q'›
  by (metis Sync_commute τ_trans_SyncL)


lemma ev_trans_SyncL : ‹e ∉ S ⟹ P ↝⇘e⇙ P' ⟹ P ⟦S⟧ Q ↝⇘e⇙ P' ⟦S⟧ Q›
  by (simp add: Aftertick_Sync initials_Sync BOT_τ_trans_anything image_iff)
    (meson τ_trans_NdetL τ_trans_SyncL τ_trans_transitivity ev_trans_is)

lemma ev_trans_SyncR : ‹e ∉ S ⟹ Q ↝⇘e⇙ Q' ⟹ P ⟦S⟧ Q ↝⇘e⇙ P ⟦S⟧ Q'›
  by (metis Sync_commute ev_trans_SyncL)

lemma ev_trans_SyncLR :
  ‹e ∈ S ⟹ P ↝⇘e⇙ P' ⟹ Q ↝⇘e⇙ Q' ⟹ P ⟦S⟧ Q ↝⇘e⇙ P' ⟦S⟧ Q'›
  by (simp add: Aftertick_Sync BOT_τ_trans_anything initials_Sync)
    (meson τ_trans_SyncL τ_trans_SyncR τ_trans_transitivity ev_trans_is)


lemmas Sync_OpSem_rules = τ_trans_SyncL τ_trans_SyncR
  ev_trans_SyncL ev_trans_SyncR
  ev_trans_SyncLR
  τ_trans_SKIP_SyncL τ_trans_SKIP_SyncR
  tick_trans_SKIP_Sync_SKIP

end



subsection ‹@{const [source] Sliding} Laws›

locale OpSemTransitionsSliding = OpSemTransitions Ψ Ω ‹(↝τ)› 
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50) +
  assumes τ_trans_SlidingL : ‹P ↝τ P' ⟹ P ⊳ Q ↝τ P' ⊳ Q›
    ―‹We just add the @{thm [source] τ_trans_SlidingL} property.›
begin

lemmas Sliding_OpSem_rules = τ_trans_SlidingR τ_trans_SlidingL
  ev_trans_SlidingL tick_trans_SlidingL

end

(* sublocale OpSemTransitionsDet ⊆ OpSemTransitionsSliding
  apply unfold_locales 
  apply (simp add: Sliding_def)

  oops

  We need an additional assumption: kind of monotony of τ_trans on both sides *)


subsection ‹@{const [source] Sliding} relaxed Laws›

―‹Introduced to recover some rules with term‹(⊑F)› refinement.›

locale OpSemTransitionsSlidingRelaxed = OpSemTransitions Ψ Ω ‹(↝τ)› 
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50) +
  assumes τ_trans_SlidingL : ‹P = ⊥ ∨ P' ≠ ⊥ ∨ Q = ⊥ ⟹ P ↝τ P' ⟹ P ⊳ Q ↝τ P' ⊳ Q›
    ―‹We just add the @{thm [source] τ_trans_SlidingL} property.›
begin

lemmas Sliding_OpSem_rules = τ_trans_SlidingR τ_trans_SlidingL
  ev_trans_SlidingL tick_trans_SlidingL

end



subsection ‹@{const [source] Interrupt} Laws›

locale OpSemTransitionsInterruptL = OpSemTransitions Ψ Ω ‹(↝τ)› 
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50) +
  assumes τ_trans_InterruptL : ‹P ↝τ P' ⟹ P △ Q ↝τ P' △ Q ›
begin

lemma ev_trans_InterruptL: ‹P ↝⇘e⇙ P' ⟹ P △ Q ↝⇘e⇙ P' △ Q›
  apply (simp add: Aftertick_Interrupt initials_Interrupt)
  using τ_trans_InterruptL τ_trans_NdetR τ_trans_transitivity by blast


(* lemma event_trans_InterruptR: ‹Q ↝e Q' ⟹ P △ Q ↝e Q'›
  oops *)
(* same issue as everywhere with Ω, we need to split *)

lemma ev_trans_InterruptR: ‹Q ↝⇘e⇙ Q' ⟹ P △ Q ↝⇘e⇙ Q'›
  apply (simp add: Aftertick_Interrupt initials_Interrupt)
  using τ_trans_NdetL τ_trans_transitivity by blast

end


locale OpSemTransitionsInterrupt = OpSemTransitionsInterruptL Ψ Ω ‹(↝τ)› 
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50) +
  assumes τ_trans_InterruptR : ‹Q ↝τ Q' ⟹ P △ Q ↝τ P △ Q'›
    ―‹We just add the @{thm [source] τ_trans_InterruptR} property.›
begin

lemmas Interrupt_OpSem_rules = τ_trans_InterruptL τ_trans_InterruptR
  ev_trans_InterruptL ev_trans_InterruptR
  tick_trans_InterruptL tick_trans_InterruptR

end



subsection ‹@{const [source] Throw} Laws›

locale OpSemTransitionsThrow = OpSemTransitions Ψ Ω ‹(↝τ)› 
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50) +
  assumes τ_trans_ThrowL : ‹P ↝τ P' ⟹ P Θ a ∈ A. Q a ↝τ P' Θ a ∈ A. Q a›
begin

(* We don't want τ_trans_ThrowR in "The expressiveness of CSP extended by priority" 
   because only the first argument is active *)

lemma ev_trans_ThrowL_notin:
  ‹e ∉ A ⟹ P ↝⇘e⇙ P' ⟹ P Θ a ∈ A. Q a ↝⇘e⇙ (P' Θ a ∈ A. Q a)›
  by (simp add: Aftertick_Throw initials_Throw BOT_τ_trans_anything τ_trans_ThrowL)

lemmas Throw_OpSem_rules = τ_trans_ThrowL tick_trans_ThrowL
  ev_trans_ThrowL_notin ev_trans_ThrowR_inside

end





section ‹Locales, Assemble !›

text ‹It is now time to assemble our locales.›

locale OpSemTransitionsAll =
  OpSemTransitionsDet Ψ Ω ‹(↝τ)› +
  OpSemTransitionsSeq Ψ Ω ‹(↝τ)› +
  OpSemTransitionsHiding Ψ Ω ‹(↝τ)› +
  OpSemTransitionsSync Ψ Ω ‹(↝τ)› +
  OpSemTransitionsSliding Ψ Ω ‹(↝τ)› +
  OpSemTransitionsInterrupt Ψ Ω ‹(↝τ)› +
  OpSemTransitionsThrow Ψ Ω ‹(↝τ)›
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50)


text ‹Of course we need to duplicate the locale for obtaining const‹Renaming› rules.›

locale OpSemTransitionsAllDuplicated = 
  OpSemTransitionsAllα: OpSemTransitionsAll Ψα Ωα ‹(α↝τ)› +
  OpSemTransitionsAllβ: OpSemTransitionsAll Ψβ Ωβ ‹(β↝τ)› +
  OpSemTransitionsRenaming Ψα Ωα τ_transα Ψβ Ωβ τ_transβ
  for Ψα :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ωα :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_transα :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹α↝τ› 50)
    and Ψβ :: ‹[('b, 's) processptick, 'b] ⇒ ('b, 's) processptick›
    and Ωβ :: ‹[('b, 's) processptick, 's] ⇒ ('b, 's) processptick›
    and τ_transβ :: ‹[('b, 's) processptick, ('b, 's) processptick] ⇒ bool› (infixl ‹β↝τ› 50)
begin

notation OpSemTransitionsAllα.ev_trans (‹_ α↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsAllα.tick_trans (‹_ α↝✓⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsAllβ.ev_trans (‹_ β↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsAllβ.tick_trans (‹_ β↝✓⇘_⇙ _› [50, 3, 51] 50)

end



section ‹‹(↝τ)› instantiated with term‹(⊑FD)› or term‹(⊑DT)››

subsection ‹‹(↝τ)› instantiated with term‹(⊑FD)››

locale OpSemFD =
  fixes Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
  assumes mono_Ω_FD: ‹✓(r) ∈ Q0 ⟹ P ⊑FD Q ⟹ Ω P r ⊑FD Ω Q r›


sublocale OpSemFD ⊆ OpSemTransitionsAll _ _ ‹(⊑FD) :: ('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool›
proof unfold_locales
  show ‹P ⊓ Q ⊑FD P› for P Q :: ‹('a, 'r) processptick› by (fact Ndet_FD_self_left)
next      
  show ‹P ⊑FD Q ⟹ Q ⊑FD R ⟹ P ⊑FD R› for P Q R :: ‹('a, 'r) processptick› by (fact trans_FD)
next
  show ‹P ⊑FD Q ⟹ Q0 ⊆ P0› for P Q :: ‹('a, 'r) processptick› by (fact anti_mono_initials_FD)
next
  show ‹e ∈ Q0 ⟹ P ⊑FD Q ⟹
        AfterExt.Aftertick Ψ Ω P e ⊑FD AfterExt.Aftertick Ψ Ω Q e› for e P Q
    by (cases e) (simp_all add: AfterExt.Aftertick_def After.mono_After_FD mono_Ω_FD)
next
  show ‹P ⊑FD P' ⟹ P □ Q ⊑FD P' □ Q› for P P' Q :: ‹('a, 'r) processptick›
    by (intro mono_Det_FD idem_FD)
next
  show ‹P ⊑FD P' ⟹ P ; Q ⊑FD P' ; Q› for P P' Q :: ‹('a, 'r) processptick›
    by (intro mono_Seq_FD idem_FD)
next
  show ‹P ⊑FD P' ⟹ P \ A ⊑FD P' \ A› for P P' :: ‹('a, 'r) processptick› and A
    by (intro mono_Hiding_FD idem_FD)
next
  show ‹P ⊑FD P' ⟹ P ⟦S⟧ Q ⊑FD P' ⟦S⟧ Q› for P P' Q :: ‹('a, 'r) processptick› and S
    by (intro mono_Sync_FD idem_FD)
next
  show ‹P ⊑FD P' ⟹ P ⊳ Q ⊑FD P' ⊳ Q› for P P' Q :: ‹('a, 'r) processptick›
    by (intro mono_Sliding_FD idem_FD)
next
  show ‹P ⊑FD P' ⟹ P △ Q ⊑FD P' △ Q› for P P' Q :: ‹('a, 'r) processptick›
    by (intro mono_Interrupt_FD idem_FD)
next
  show ‹Q ⊑FD Q' ⟹ P △ Q ⊑FD P △ Q'› for P Q Q' :: ‹('a, 'r) processptick›
    by (intro mono_Interrupt_FD idem_FD)
next
  show ‹P ⊑FD P' ⟹ P Θ a ∈ A. Q a ⊑FD P' Θ a ∈ A. Q a› for P P' :: ‹('a, 'r) processptick› and  A Q
    by (intro mono_Throw_FD idem_FD)
qed



context OpSemFD
begin

text ‹Finally, the only remaining hypothesis is @{thm mono_Ω_FD} when we instantiate our locale
      with the failure-divergence refinement term‹(⊑FD)›.›

text ‹Of course, we can strengthen some previous results.›

(* no_notation failure_divergence_refine (infix ‹⊑FD› 60) *)

notation failure_divergence_refine (infixl ‹FD↝τ› 50)
notation ev_trans (‹_ FD↝⇘_⇙ _› [50, 3, 51] 50)
notation tick_trans (‹_ FD↝✓⇘_⇙ _› [50, 3, 51] 50)
notation trace_trans (‹_ FD↝*_ _› [50, 3, 51] 50)


lemma trace_trans_imp_F: ‹P FD↝*s Q ⟹ X ∈ ℛ Q ⟹ (s, X) ∈ ℱ P›
  by (rule trace_trans_imp_F_if_τ_trans_imp_leF) (simp add: leFD_imp_leF)

lemma tickFree_trace_trans_BOT_imp_D: ‹tickFree s ⟹ P FD↝*s ⊥ ⟹ s ∈ 𝒟 P›
  by (rule tickFree_trace_trans_BOT_imp_D_if_τ_trans_BOT_imp_eq_BOT_weak) (simp add: FD_antisym)

lemma F_trace_trans_reality_check: ‹tickFree s ⟹ (s, X) ∈ ℱ P ⟷ (∃Q. (P FD↝*s Q) ∧ X ∈ ℛ Q)›
  by (simp add: F_trace_trans_reality_check_weak leFD_imp_leF)

lemma D_trace_trans_reality_check: ‹tickFree s ⟹ s ∈ 𝒟 P ⟷ P FD↝*s ⊥›
  by (simp add: D_trace_trans_reality_check_weak FD_antisym)


lemma Ω_SKIP_is_STOP_imp_SKIP_trace_trans_iff: 
  ‹Ω (SKIP r) r = STOP ⟹ (SKIP r FD↝*s P) ⟷ s = [] ∧ P = SKIP r ∨ s = [✓(r)] ∧ P = STOP›
  by (erule Ω_SKIP_is_STOP_imp_τ_trans_imp_leF_imp_SKIP_trace_trans_iff)
    (simp add: leFD_imp_leF)


lemmas τ_trans_adm = le_FD_adm 

lemma ev_trans_adm[simp]:
  ‹⟦cont (λP. Ψ P e); cont u; monofun v⟧ ⟹ adm (λx. u x FD↝⇘e⇙ v x)›
  by simp

lemma tick_trans_adm[simp]:
  ‹⟦cont (λP. Ω P r); cont u; monofun v⟧ ⟹ adm (λx. u x FD↝✓⇘r⇙ v x)›
  by simp


lemma trace_trans_adm[simp]:
  ‹⟦∀x. ev x ∈ set s ⟶ cont (λP. Ψ P x);
    ∀r. ✓(r) ∈ set s ⟶ cont (λP. Ω P r); cont u; monofun v⟧
   ⟹ adm (λx. u x FD↝*s (v x))›
  by simp

end

locale OpSemFDDuplicated =
  OpSemFDα: OpSemFD Ψα Ωα + OpSemFDβ: OpSemFD Ψβ Ωβ
  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 OpSemFDDuplicated ⊆ OpSemTransitionsAllDuplicated _ _ ‹(⊑FD)› _ _ ‹(⊑FD)›
  by (unfold_locales) (simp add: mono_Renaming_FD)




subsection ‹‹(↝τ)› instantiated with term‹(⊑DT)››

locale OpSemDT =
  fixes Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
  assumes mono_Ω_DT: ‹✓(r) ∈ Q0 ⟹ P ⊑DT Q ⟹ Ω P r ⊑DT Ω Q r›


sublocale OpSemDT ⊆ OpSemTransitionsAll _ _ ‹(⊑DT) :: ('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool›
proof unfold_locales
  show ‹P ⊓ Q ⊑DT P› for P Q :: ‹('a, 'r) processptick› by (fact Ndet_DT_self_left)
next      
  show ‹P ⊑DT Q ⟹ Q ⊑DT R ⟹ P⊑DT R› for P Q R :: ‹('a, 'r) processptick› by (fact trans_DT)
next
  show ‹P ⊑DT Q ⟹ Q0 ⊆ P0› for P Q :: ‹('a, 'r) processptick› by (fact anti_mono_initials_DT)
next
  show ‹e ∈ Q0 ⟹ P ⊑DT Q ⟹
        AfterExt.Aftertick Ψ Ω P e ⊑DT AfterExt.Aftertick Ψ Ω Q e› for e P Q
    by (cases e) (simp_all add: AfterExt.Aftertick_def After.mono_After_DT mono_Ω_DT)
qed (simp_all add: mono_Det_DT mono_Seq_DT mono_Hiding_DT mono_Sync_DT
    mono_Sliding_DT mono_Interrupt_DT mono_Throw_DT)


context OpSemDT
begin

text ‹Finally, the only remaining hypothesis is @{thm mono_Ω_DT} when we instantiate our locale
      with the failure-divergence refinement term‹(⊑DT)›.›

text ‹Of course, we can strengthen some previous results.›

(* no_notation failure_divergence_refine (infix ‹⊑DT› 60) *)

notation trace_divergence_refine (infixl ‹DT↝τ› 50)
notation ev_trans (‹_ DT↝⇘_⇙ _› [50, 3, 51] 50)
notation tick_trans (‹_ DT↝✓⇘_⇙ _› [50, 3, 51] 50)
notation trace_trans (‹_ DT↝*_ _› [50, 3, 51] 50)


lemma tickFree_trace_trans_BOT_imp_D: ‹tickFree s ⟹ P DT↝*s ⊥ ⟹ s ∈ 𝒟 P›
  by (rule tickFree_trace_trans_BOT_imp_D_if_τ_trans_BOT_imp_eq_BOT_weak)
    (meson BOT_iff_Nil_D divergence_refine_def leDT_imp_leD subsetD)

lemma D_trace_trans_reality_check: ‹tickFree s ⟹ s ∈ 𝒟 P ⟷ P DT↝*s ⊥›
  by (simp add: D_trace_trans_reality_check_weak BOT_iff_Nil_D tickFree_trace_trans_BOT_imp_D trace_τ_trans)


lemmas τ_trans_adm = le_DT_adm 

lemma ev_trans_adm[simp]:
  ‹⟦cont (λP. Ψ P e); cont u; monofun v⟧ ⟹ adm (λx. u x DT↝⇘e⇙ v x)›
  by simp


lemma tick_trans_adm[simp]:
  ‹⟦cont (λP. Ω P r); cont u; monofun v⟧ ⟹ adm (λx. u x DT↝✓⇘r⇙ v x)›
  by simp


lemma trace_trans_adm[simp]:
  ‹⟦∀x. ev x ∈ set s ⟶ cont (λP. Ψ P x);
    ∀r. ✓(r) ∈ set s ⟶ cont (λP. Ω P r); cont u; monofun v⟧
   ⟹ adm (λx. u x DT↝*s (v x))›
  by simp


text ‹If we only look at the traces and the divergences, non-deterministic and deterministic 
      choices are the same. Therefore we can obtain even stronger results for the operational rules.›

lemma τ_trans_Det_is_τ_trans_Ndet: ‹P □ Q DT↝τ R ⟷ P ⊓ Q DT↝τ R›
  unfolding trace_divergence_refine_def trace_refine_def divergence_refine_def
  by (simp add: T_Det T_Ndet D_Det D_Ndet)

lemma τ_trans_Sliding_is_τ_trans_Ndet: ‹P ⊳ Q DT↝τ R ⟷ P ⊓ Q DT↝τ R›
  unfolding Sliding_def by (metis Det_assoc Det_id τ_trans_Det_is_τ_trans_Ndet)

end

locale OpSemDTDuplicated =
  OpSemDTα: OpSemDT Ψα Ωα + OpSemDTβ: OpSemDT Ψβ Ωβ
  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 OpSemDTDuplicated ⊆ OpSemTransitionsAllDuplicated _ _ ‹(⊑DT)› _ _ ‹(⊑DT)›
  by (unfold_locales) (simp add: mono_Renaming_DT)




section ‹‹(↝τ)› instantiated with term‹(⊑F)› or term‹(⊑T)››

text ‹We will only recover the rules for some operators.›

subsection ‹‹(↝τ)› instantiated with term‹(⊑F)››

locale OpSemF =
  fixes Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
  assumes mono_Ω_F: ‹✓(r) ∈ Q0 ⟹ P ⊑F Q ⟹ Ω P r ⊑F Ω Q r›

sublocale OpSemF ⊆ OpSemTransitionsHiding _ _ ‹(⊑F) :: ('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool› +
  OpSemTransitionsDetRelaxed _ _ ‹(⊑F) :: ('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool› +
  OpSemTransitionsSlidingRelaxed _ _ ‹(⊑F) :: ('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool›
proof unfold_locales
  show ‹P ⊓ Q ⊑F P› for P Q :: ‹('a, 'r) processptick› by (fact Ndet_F_self_left)
next      
  show ‹P ⊑F Q ⟹ Q ⊑F R ⟹ P⊑F R› for P Q R :: ‹('a, 'r) processptick› by (fact trans_F)
next
  show ‹P ⊑F Q ⟹ Q0 ⊆ P0› for P Q :: ‹('a, 'r) processptick› by (fact anti_mono_initials_F)
next
  show ‹e ∈ Q0 ⟹ P ⊑F Q ⟹
        AfterExt.Aftertick Ψ Ω P e ⊑F AfterExt.Aftertick Ψ Ω Q e› for e P Q
    by (cases e) (simp_all add: AfterExt.Aftertick_def After.mono_After_F mono_Ω_F)
qed (simp_all add: non_BOT_mono_Det_left_F non_BOT_mono_Sliding_F mono_Hiding_F)


context OpSemF
begin

notation failure_refine (infixl ‹F↝τ› 50)
notation ev_trans (‹_ F↝⇘_⇙ _› [50, 3, 51] 50)
notation tick_trans (‹_ F↝✓⇘_⇙ _› [50, 3, 51] 50)
notation trace_trans (‹_ F↝*_ _› [50, 3, 51] 50)

text ‹For @{const [source] Det} and @{const [source] Sliding},
      we have relaxed versions on ‹τ› transitions.›

end

text ‹By duplicating the locale, we can recover a rules for const‹Renaming›.›

locale OpSemFDuplicated =
  OpSemFα: OpSemF Ψα Ωα + OpSemFβ: OpSemF Ψβ Ωβ
  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 OpSemFDuplicated ⊆ OpSemTransitionsDuplicated _ _ ‹(⊑F)› _ _ ‹(⊑F)›
  by unfold_locales

context OpSemFDuplicated
begin

notation OpSemFα.ev_trans (‹_ αF↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemFα.tick_trans (‹_ αF↝✓⇘_⇙ _› [50, 3, 51] 50)
notation OpSemFβ.ev_trans (‹_ βF↝⇘_⇙ _› [50, 3, 51] 50) 
notation OpSemFβ.tick_trans (‹_ βF↝✓⇘_⇙ _› [50, 3, 51] 50)

end


context OpSemF
begin

lemma trace_trans_imp_F: ‹P F↝*s Q ⟹ X ∈ ℛ Q ⟹ (s, X) ∈ ℱ P›
  by (rule trace_trans_imp_F_if_τ_trans_imp_leF) simp


lemma Ω_SKIP_is_STOP_imp_SKIP_trace_trans_iff: 
  ‹Ω (SKIP r) r = STOP ⟹ (SKIP r F↝*s P) ⟷ s = [] ∧ P = SKIP r ∨ s = [✓(r)] ∧ P = STOP›
  by (erule Ω_SKIP_is_STOP_imp_τ_trans_imp_leF_imp_SKIP_trace_trans_iff) simp



lemmas τ_trans_adm = le_F_adm 

lemma ev_trans_adm[simp]:
  ‹⟦cont (λP. Ψ P e); cont u; monofun v⟧ ⟹ adm (λx. u x F↝⇘e⇙ v x)›
  by simp

lemma tick_trans_adm[simp]:
  ‹⟦cont (λP. Ω P r); cont u; monofun v⟧ ⟹ adm (λx. u x F↝✓⇘r⇙ v x)›
  by simp


lemma trace_trans_adm[simp]:
  ‹⟦∀x. ev x ∈ set s ⟶ cont (λP. Ψ P x);
    ∀r. ✓(r) ∈ set s ⟶ cont (λP. Ω P r);
    cont u; monofun v⟧ ⟹ adm (λx. u x F↝*s (v x))›
  by simp

end


subsection ‹‹(↝τ)› instantiated with term‹(⊑T)››

locale OpSemTransitionsForT = 
  OpSemTransitionsDet Ψ Ω ‹(↝τ)› +
  OpSemTransitionsHiding Ψ Ω ‹(↝τ)› +
  OpSemTransitionsSliding Ψ Ω ‹(↝τ)› +
  OpSemTransitionsInterrupt Ψ Ω ‹(↝τ)›
  for Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_trans :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹↝τ› 50)

locale OpSemT =
  fixes Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ω :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
  assumes mono_Ω_T: ‹✓(r) ∈ Q0 ⟹ P ⊑T Q ⟹ Ω P r ⊑T Ω Q r›

sublocale OpSemT ⊆ OpSemTransitionsForT _ _ ‹(⊑T) :: ('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool›
proof unfold_locales
  show ‹P ⊓ Q ⊑T P› for P Q :: ‹('a, 'r) processptick› by (fact Ndet_T_self_left)
next      
  show ‹P ⊑T Q ⟹ Q ⊑T R ⟹ P⊑T R› for P Q R :: ‹('a, 'r) processptick› by (fact trans_T)
next
  show ‹P ⊑T Q ⟹ Q0 ⊆ P0› for P Q :: ‹('a, 'r) processptick› by (fact anti_mono_initials_T)
next
  show ‹e ∈ Q0 ⟹ P ⊑T Q ⟹
        AfterExt.Aftertick Ψ Ω P e ⊑T AfterExt.Aftertick Ψ Ω Q e› for e P Q
    by (cases e) (simp_all add: AfterExt.Aftertick_def After.mono_After_T mono_Ω_T)
qed (simp_all add: mono_Det_T mono_Sliding_T mono_Hiding_T mono_Interrupt_T)

context OpSemT
begin

notation trace_refine (infixl ‹T↝τ› 50)
notation ev_trans (‹_ T↝⇘_⇙ _› [50, 3, 51] 50)
notation tick_trans (‹_ T↝✓⇘_⇙ _› [50, 3, 51] 50)
notation trace_trans (‹_ T↝*_ _› [50, 3, 51] 50)

end

text ‹By duplicating the locale, we can recover a rules for const‹Renaming›.›

locale OpSemTDuplicated =
  OpSemTα: OpSemT Ψα Ωα + OpSemTβ: OpSemT Ψβ Ωβ
  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 OpSemTDuplicated ⊆ OpSemTransitionsDuplicated _ _ ‹(⊑T)› _ _ ‹(⊑T)›
  by unfold_locales

context OpSemTDuplicated
begin

notation OpSemTα.ev_trans (‹_ αT↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTα.tick_trans (‹_ αT↝✓⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTβ.ev_trans (‹_ βT↝⇘_⇙ _› [50, 3, 51] 50) 
notation OpSemTβ.tick_trans (‹_ βT↝✓⇘_⇙ _› [50, 3, 51] 50)


end


context OpSemT
begin

lemmas τ_trans_adm = le_T_adm 

lemma ev_trans_adm[simp]:
  ‹⟦cont (λP. Ψ P e); cont u; monofun v⟧ ⟹ adm (λx. u x T↝⇘e⇙ v x)›
  by simp

lemma tick_trans_adm[simp]:
  ‹⟦cont (λP. Ω P r); cont u; monofun v⟧ ⟹ adm (λx. u x T↝✓⇘r⇙ v x)›
  by simp

lemma trace_trans_adm[simp]:
  ‹⟦∀x. ev x ∈ set s ⟶ cont (λP. Ψ P x);
    ∀r. ✓(r) ∈ set s ⟶ cont (λP. Ω P r); cont u; monofun v⟧
   ⟹ adm (λx. u x T↝*s (v x))›
  by simp


text ‹If we only look at the traces, non-deterministic and deterministic choices are the same.
      Therefore we can obtain even stronger results for the operational rules.›

lemma τ_trans_Det_is_τ_trans_Ndet: ‹P □ Q T↝τ R ⟷ P ⊓ Q T↝τ R›
  unfolding trace_divergence_refine_def trace_refine_def divergence_refine_def
  by (simp add: T_Det T_Ndet D_Det D_Ndet)

lemma τ_trans_Sliding_is_τ_trans_Ndet: ‹P ⊳ Q T↝τ R ⟷ P ⊓ Q T↝τ R›
  unfolding Sliding_def by (metis Det_assoc Det_id τ_trans_Det_is_τ_trans_Ndet)


end

(*<*)
end
  (*>*)