Theory OpSemGeneric

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : Common work for operational semantics based on refinements
 *
 * Copyright (c) 2023 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  OpSemGeneric
  imports AfterTrace
begin

section ‹Definition›

text ‹We define a correspondence pattern using a locale in order to factorize the redundant proofs.›

locale OpSemGeneric = 
    fixes τ_trans :: ‹['α process, 'α process] ⇒ bool› (infixl ‹↝⇩τ› 50)
  assumes τ_trans_NdetL: ‹P ⊓ Q ↝⇩τ P›
      and τ_trans_transitivity: ‹P ↝⇩τ Q ⟹ Q ↝⇩τ R ⟹ P ↝⇩τ R›
      and τ_trans_anti_mono_ready_set: ‹P ↝⇩τ Q ⟹ ready_set Q ⊆ ready_set P›
      and τ_trans_mono_AfterExt:
          ‹e ∈ ready_set Q ⟹ P ↝⇩τ Q ⟹ P afterExt e ↝⇩τ Q afterExt e›
begin

text ‹This locale needs to be instantiated with a binary
      relation @{term [show_types] ‹(↝⇩τ)›} which:
      ▪ is compatible with \<^const>‹Ndet›
      ▪ is transitive
      ▪ makes \<^const>‹ready_set› anti-monotonic
      ▪ makes @{const [source] AfterExt} monotonic.›

text ‹From the ‹τ› transition \<^term>‹P ↝⇩τ Q› we derive the event transition as follows:›

abbreviation event_trans :: ‹['α process, 'α event, 'α process] ⇒ bool› 
                           (‹_/ ↝_/ _› [50, 3, 51] 50)
  where ‹P ↝e Q ≡ e ∈ ready_set P ∧ P afterExt e ↝⇩τ Q›


text ‹From idempotence, commutativity and \<^term>‹⊥› absorbance 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›
  and BOT_event_trans_anything: ‹⊥ ↝e P›
  by (metis Ndet_id τ_trans_NdetL,
      metis Ndet_commute τ_trans_NdetL,
      metis Ndet_BOT τ_trans_NdetL,
      metis AfterExt_BOT Ndet_BOT UNIV_I τ_trans_NdetL ready_set_BOT) 


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

lemma event_trans_τ_trans: ‹P ↝ e P' ⟹ P' ↝⇩τ P''  ⟹ P ↝ e P''›
  by (meson τ_trans_transitivity)

lemma τ_trans_event_trans: ‹P ↝⇩τ P'  ⟹ P' ↝ e P'' ⟹ P ↝ e P''›
  using τ_trans_mono_AfterExt τ_trans_transitivity τ_trans_anti_mono_ready_set by blast



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

inductive trace_trans :: ‹'α process ⇒ 'α trace ⇒ 'α process ⇒ bool›
                        (‹_/ ↝⇧*_/ _› [50, 3, 51] 50)
  where    trace_τ_trans : ‹P ↝⇩τ P' ⟹ P ↝⇧* [] P'›
  |     trace_tick_trans : ‹P ↝✓  P' ⟹ P ↝⇧* [✓] P'›
  |  trace_Cons_ev_trans :
     ‹P ↝(ev 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)
  subgoal using τ_trans_transitivity trace_τ_trans by blast
  subgoal using event_trans_τ_trans trace_tick_trans by 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)
  subgoal using τ_trans_transitivity trace_τ_trans by blast
  subgoal using τ_trans_event_trans trace_tick_trans by blast
  using τ_trans_event_trans trace_Cons_ev_trans by blast


lemma BOT_trace_trans_anything : ‹front_tickFree s ⟹ ⊥ ↝⇧*s P›
proof (induct s arbitrary: P)
  show ‹⋀P. front_tickFree [] ⟹ ⊥ ↝⇧*[] P›
    by (simp add: BOT_τ_trans_anything trace_τ_trans)
next
  fix e s P
  assume prem: ‹front_tickFree (e # s)› and hyp: ‹front_tickFree s ⟹ ⊥ ↝⇧*s P› for P
  have * : ‹front_tickFree s› 
    by (metis prem butlast.simps(2) front_tickFree_butlast front_tickFree_def tickFree_Cons)
  show ‹⊥ ↝⇧*e # s P›
  proof (cases e)
    fix e'
    assume ‹e = ev e'›
    show ‹⊥ ↝⇧*e # s P›
      by (simp add: ‹e = ev e'›)
         (rule trace_Cons_ev_trans[OF _ hyp];
          simp add: * AfterExt_BOT BOT_τ_trans_anything ready_set_BOT)
  next
    have ‹e = ✓ ⟹ s = []› 
      by (metis prem butlast.simps(2) front_tickFree_butlast tickFree_Cons)
    thus ‹e = ✓ ⟹ ⊥ ↝⇧*e # s P› 
      by (simp add: AfterExt_BOT BOT_τ_trans_anything ready_set_BOT trace_tick_trans)
  qed
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 ↝✓ Q ⟹ X ∈ ℛ Q ⟹ ([✓], X) ∈ ℱ P› for P Q
    by (metis append_Nil mem_Collect_eq ready_set_def tick_T_F)
next
  fix P e Q s Q'
  assume * : ‹P ↝(ev e) Q› ‹X ∈ ℛ Q' ⟹ (s, X) ∈ ℱ Q› ‹X ∈ ℛ Q'›
  have ‹P afterExt ev e ⊑⇩F Q› using *(1) that by blast
  hence ‹(s, X) ∈ ℱ (P afterExt ev e)› by (simp add: failure_refine_def subsetD *(2, 3))
  thus ‹(ev e # s, X) ∈ ℱ P› by (simp add: F_AfterExt *(1)) (metis list.exhaust_sel)
qed


lemma trace_trans_imp_T_if_τ_trans_imp_leT: ‹P ↝⇧*s Q ⟹ s ∈ 𝒯 P› 
  if ‹∀P Q. P ↝⇩τ Q ⟶ P ⊑⇩T Q›
proof (induct rule: trace_trans.induct)
  show ‹P ↝⇩τ Q ⟹ [] ∈ 𝒯 P› for P Q
    by (simp add: Nil_elem_T)
next
  show ‹P ↝✓ Q ⟹ [✓] ∈ 𝒯 P› for P Q
    by (simp add: ready_set_def)
next
  fix P e Q s Q'
  assume * : ‹P ↝(ev e) Q› ‹s ∈ 𝒯 Q›
  have ‹P afterExt ev e ⊑⇩T Q› using *(1) that by blast
  hence ‹s ∈ 𝒯 (P afterExt ev e)› by (simp add: *(2) subsetD trace_refine_def)
  with *(1) list.collapse show ‹ev e # s ∈ 𝒯 P› 
    by (force simp add: T_AfterExt ready_set_def)
qed


lemma trace_trans_BOT_imp_D_if_τ_trans_imp_leD: ‹P ↝⇧*s ⊥ ⟹ s ∈ 𝒟 P› 
  if ‹∀P Q. P ↝⇩τ Q ⟶ P ⊑⇩D Q›
proof (induct s arbitrary: P)
  show ‹⋀P. P ↝⇧*[] ⊥ ⟹ [] ∈ 𝒟 P›
    by (subst (asm) trace_trans.simps, auto) 
       (meson BOT_iff_D divergence_refine_def subsetD that)
next
  fix e s P
  assume prem : ‹P ↝⇧*e # s ⊥› 
  assume hyp: ‹P ↝⇧*s ⊥ ⟹ s ∈ 𝒟 P› for P
  have ‹P afterExt e ↝⇧*s ⊥›
    using prem by (cases rule: trace_trans.cases)
                  (auto simp add:  trace_τ_trans intro: τ_trans_trace_trans)
  from hyp[OF this] show ‹e # s ∈ 𝒟 P›
    by (fastforce intro: prem trace_trans.cases simp add: D_AfterExt D_UU split: if_split_asm )
qed



section ‹Characterizations for \<^term>‹P ↝⇧*s Q››

lemma trace_trans_iff :
  ‹P ↝⇧* [] Q ⟷ P ↝⇩τ Q›
  ‹P ↝⇧* [✓] Q ⟷ P ↝✓ Q›
  ‹P ↝⇧* (ev e) # s Q' ⟷ (∃Q. P ↝(ev e) Q ∧ Q ↝⇧* s Q')›
  ‹tickFree s ⟹ (P ↝⇧* s @ [f] Q') ⟷ (∃Q. P ↝⇧*s Q ∧ Q ↝f 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 ↝⇧* [✓] Q ⟷ P ↝✓  Q›
   and f3 : ‹⋀P Q' e. P ↝⇧* (ev e) # s Q' ⟷ (∃Q. P ↝(ev e) Q ∧ Q ↝⇧* s Q')›
    by ((subst trace_trans.simps, auto)[1])+
   
  show f4 : ‹tickFree s ⟹ (P ↝⇧* s @ [f] Q') ⟷ (∃Q. P ↝⇧*s Q ∧ Q ↝f Q')› for s f P Q'
  proof safe
    show ‹P ↝⇧* s @ [f] Q' ⟹ ∃Q. P ↝⇧*s Q ∧ Q ↝f Q'›
    proof (induct s arbitrary: P)
      case Nil
      thus ?case 
        apply (subst (asm) trace_trans.simps, simp)
        using τ_trans_eq τ_trans_transitivity f1 by blast
    next
      case (Cons e s)
      from Cons.prems have * : ‹e ∈ ready_set P ∧ P afterExt e ↝⇧*s @ [f] Q'›
        by (subst (asm) trace_trans.simps)
           (auto simp add:  intro: τ_trans_trace_trans)
      with Cons.hyps obtain Q where ** : ‹P afterExt e ↝⇧*s Q› ‹Q ↝f 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 = ✓ ⟹ s = []› by (subst (asm) trace_trans.simps) auto
        thus ‹e = ✓ ⟹ P ↝⇧*e # s Q› using * **(1) f1 f2 by blast
      qed
      with "**"(2) show ‹∃Q. P ↝⇧*e # s Q ∧ Q ↝f Q'› by blast
    qed
  next
    show ‹tickFree s ⟹ P ↝⇧*s Q ⟹ f ∈ ready_set Q ⟹ Q afterExt f ↝⇩τ Q' ⟹
          P ↝⇧*s @ [f] Q'› for Q
    proof (induct s arbitrary: P Q)
      show ‹tickFree [] ⟹ P ↝⇧*[] Q ⟹ f ∈ ready_set Q ⟹ Q afterExt f ↝⇩τ Q' ⟹ 
            P ↝⇧*[] @ [f] Q'› for P Q
        by (simp add: f1)
           (metis (full_types) τ_trans_eq τ_trans_event_trans event.exhaust 
                               trace_Cons_ev_trans trace_τ_trans trace_tick_trans)
    next
      case (Cons e s)
      from Cons.prems(2) have * : ‹e ∈ ready_set P ∧ P afterExt 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'› 
          apply simp
          by (rule trace_Cons_ev_trans
                   [OF _ Cons.hyps[OF tickFree_tl[OF Cons.prems(1), simplified] 
                                      *[THEN conjunct2] Cons.prems(3)]])
             (use * τ_trans_eq Cons.prems(4) in ‹blast+›)
      next
        show ‹e = ✓ ⟹ P ↝⇧*(e # s) @ [f] Q'› 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)
    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 assm obtain Q where ‹P ↝⇧*s @ t Q› ‹Q ↝e Q'›
        by (metis append.assoc f4 front_tickFree_implies_tickFree snoc.prems)
      also obtain R where ** : ‹P ↝⇧*s R› ‹R ↝⇧*t Q›
        by (metis calculation(1) append.assoc front_tickFree_dw_closed snoc.hyps snoc.prems)
      ultimately show ‹∃Q. P ↝⇧*s Q ∧ Q ↝⇧*t @ [e] Q'›
        by (metis append_is_Nil_conv f4 front_tickFree_mono list.distinct(1) snoc.prems)
    next
      assume ‹∃Q. P ↝⇧*s Q ∧ Q ↝⇧*t @ [e] Q'›
      then obtain Q where ‹P ↝⇧*s Q› ‹Q ↝⇧*t @ [e] Q'› by blast
      also obtain R where ‹Q ↝⇧*t R› ‹R ↝e Q'›
        by (metis append_is_Nil_conv calculation(2) f4
                  front_tickFree_mono list.distinct(1) snoc.prems)
      ultimately show ‹P ↝⇧*s @ t @ [e] Q'›
        by (metis append_assoc f4 front_tickFree_implies_tickFree snoc.hyps
                  snoc.prems tickFree_implies_front_tickFree)
    qed
  qed
qed



section ‹Finally: \<^term>‹P ↝⇧*s Q› is \<^term>‹P afterTrace s ↝⇩τ Q››

theorem T_imp_trace_trans_iff_AfterTrace_τ_trans : 
  ‹s ∈ 𝒯 P ⟹ (P ↝⇧*s Q) ⟷ P afterTrace s ↝⇩τ Q›
proof (intro iffI)
  show ‹P ↝⇧*s Q ⟹ s ∈ 𝒯 P ⟹ P afterTrace s ↝⇩τ Q›
  proof (induct s arbitrary: P Q rule: rev_induct)
    show ‹⋀P Q. P ↝⇧*[] Q ⟹ [] ∈ 𝒯 P ⟹ P afterTrace [] ↝⇩τ Q›
      using trace_trans.cases by auto
  next
    fix s e P Q
    assume   hyp : ‹P ↝⇧*s Q ⟹ s ∈ 𝒯 P ⟹ P afterTrace s ↝⇩τ Q› for P Q
    assume prems : ‹P ↝⇧*s @ [e] Q› ‹s @ [e] ∈ 𝒯 P›
    have * : ‹e ∈ ready_set (P afterTrace s)› 
      using prems(2) ready_set_AfterTrace by blast
    show ‹P afterTrace (s @ [e]) ↝⇩τ Q›
      by (metis AfterTrace_snoc τ_trans_event_trans append_single_T_imp_tickFree 
                hyp is_processT3_ST prems trace_trans_iff(4))
  qed
next
  show ‹P afterTrace s ↝⇩τ Q ⟹ s ∈ 𝒯 P ⟹ P ↝⇧*s Q›
  proof (induct arbitrary: P Q rule: AfterTrace.induct)
    show ‹⋀P Q. P afterTrace [] ↝⇩τ Q ⟹ [] ∈ 𝒯 P ⟹ P ↝⇧*[] Q›
      by (simp add: trace_τ_trans)
  next
    fix e and s :: ‹'α trace› and Q P
    assume   hyp : ‹P afterTrace s ↝⇩τ Q ⟹ s ∈ 𝒯 P ⟹ P ↝⇧*s Q› for P Q
    assume prems : ‹P afterTrace (e # s) ↝⇩τ Q› ‹e # s ∈ 𝒯 P›
    have * : ‹e ∈ ready_set P ∧ s ∈ 𝒯 (P afterExt e)›
      by (metis AfterTrace.simps(1, 2) Cons_in_T_imp_elem_ready_set 
                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 ↝(ev e') P afterExt (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 = ✓ ⟹ s = []› by (metis butlast.simps(2) front_tickFree_butlast 
                                           is_processT2_TR tickFree_Cons prems(2))
      thus ‹e = ✓ ⟹ P ↝⇧*e # s Q› 
        using * prems(1) trace_tick_trans by force
    qed
  qed
qed


text ‹As corollaries we obtain the reciprocal results of 

      @{thm trace_trans_imp_F_if_τ_trans_imp_leF
            trace_trans_imp_T_if_τ_trans_imp_leT
            trace_trans_BOT_imp_D_if_τ_trans_imp_leD}›

lemma F_imp_exists_trace_trans: ‹(s, X) ∈ ℱ P ⟹ ∃Q. (P ↝⇧*s Q) ∧ X ∈ ℛ Q›
  by (meson F_T F_imp_R_AfterTrace T_imp_trace_trans_iff_AfterTrace_τ_trans τ_trans_eq)

lemma T_imp_exists_trace_trans: ‹s ∈ 𝒯 P ⟹ ∃Q. P ↝⇧*s Q›
  using F_imp_exists_trace_trans T_F by blast

lemma D_imp_trace_trans_BOT: ‹s ∈ 𝒟 P ⟹ P ↝⇧*s ⊥›
  by (subst T_imp_trace_trans_iff_AfterTrace_τ_trans, simp add: D_T)
     (metis BOT_iff_D D_AfterTrace τ_trans_eq self_append_conv)
 



text ‹When we have more information on \<^term>‹P ↝⇩τ Q›, we obtain:›

lemma τ_trans_imp_leT_imp_STOP_trace_trans_iff: 
  ‹∀P Q. P ↝⇩τ Q ⟶ P ⊑⇩T Q ⟹ STOP ↝⇧*s P ⟷ s = [] ∧ P = STOP›
  using STOP_T_iff by (subst trace_trans.simps)
                      (auto simp add: ready_set_STOP τ_trans_eq) 


lemma τ_trans_imp_leF_imp_SKIP_trace_trans_iff: 
  ‹∀P Q. P ↝⇩τ Q ⟶ P ⊑⇩F Q ⟹ 
   SKIP ↝⇧*s P ⟷ s = [] ∧ P = SKIP ∨ s = [✓] ∧ P = STOP›
  using SKIP_F_iff STOP_F_iff by (subst trace_trans.simps)
                                 (auto simp add: AfterExt_SKIP ready_set_SKIP τ_trans_eq)
  
  
lemma τ_trans_imp_leT_imp_trace_trans_ready_set_subset_ready_set_AfterTrace:
  ‹∀P Q. P ↝⇩τ Q ⟶ P ⊑⇩T Q ⟹ P ↝⇧*s Q ⟹
   ready_set Q ⊆ ready_set (P afterTrace s)›
  using T_imp_trace_trans_iff_AfterTrace_τ_trans 
        anti_mono_ready_set_T trace_trans_imp_T_if_τ_trans_imp_leT by blast


lemma τ_trans_imp_leT_imp_trace_trans_imp_ready_set:
  ‹∀P Q. P ↝⇩τ Q ⟶ P ⊑⇩T Q ⟹ P ↝⇧*(s @ e # t) Q ⟹ 
   e ∈ ready_set (P afterTrace s)›
  using ready_set_AfterTrace trace_trans_imp_T_if_τ_trans_imp_leT by blast


lemma trace_trans_iff_T_and_AfterTrace_τ_trans_if_τ_trans_imp_leT: 
  ‹∀P Q. P ↝⇩τ Q ⟶ P ⊑⇩T Q ⟹
   (P ↝⇧*s Q) ⟷ s ∈ 𝒯 P ∧ P afterTrace s ↝⇩τ Q›
  using T_imp_trace_trans_iff_AfterTrace_τ_trans trace_trans_imp_T_if_τ_trans_imp_leT by blast
  


section ‹General Rules of Operational Semantics›

text ‹Some rules of operational semantics are consequences of \<^locale>‹OpSemGeneric›'s
      axioms without needing to specify more what \<^term>‹P ↝⇩τ Q› is.›

lemma SKIP_trans_tick: ‹SKIP ↝✓ STOP›
  by (simp add: AfterExt_SKIP τ_trans_eq ready_set_SKIP)

lemma tick_trans_imp_BOT_L_or_STOP_R: ‹P ↝✓ Q ⟹ P = ⊥ ∨ Q = STOP›
  by (metis τ_trans_anti_mono_ready_set ready_set_AfterExt ready_set_empty_iff_STOP subset_empty)

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



lemma ready_tick_imp_τ_trans_SKIP: ‹P ↝⇩τ SKIP› if ‹✓ ∈ ready_set P›
proof -
  from that have ‹P ⊑⇩F⇩D SKIP›
    unfolding failure_divergence_refine_def le_ref_def
    by (auto simp add: F_SKIP D_SKIP subset_iff ready_set_def is_processT6_S2)
       (metis append_Nil tick_T_F)
  then obtain Q where ‹P = Q ⊓ SKIP›
    by (metis mono_Ndet_FD mono_Ndet_FD_left FD_antisym Ndet_id idem_FD)
  thus ‹P ↝⇩τ SKIP› by (simp add: τ_trans_NdetR)
qed
 

lemma exists_tick_trans_is_ready_tick: ‹(∃P'. P ↝✓ P') ⟷ ✓ ∈ ready_set P›
  using τ_trans_eq by blast



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

lemma SKIP_cant_ev_trans: ‹¬ SKIP ↝(ev e) STOP›
  by (simp add: ready_set_SKIP)

lemma STOP_cant_event_trans: ‹¬ STOP ↝e P›
  by (simp add: ready_set_STOP)




lemma ev_trans_Mprefix: ‹e ∈ A ⟹ □a ∈ A → P a ↝(ev e) (P e)›
  by (simp add: AfterExt_def After_Mprefix τ_trans_eq ready_set_Mprefix)

lemma ev_trans_Mndetprefix: ‹e ∈ A ⟹ ⊓a ∈ A → P a ↝(ev e) (P e)›
  by (simp add: AfterExt_def After_Mndetprefix τ_trans_eq ready_set_Mndetprefix)

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



lemma τ_trans_MultiNdet: ‹finite A ⟹ x ∈ A ⟹ (⨅a ∈ A. P a) ↝⇩τ P x›
  by (metis MultiNdet_insert' τ_trans_NdetL emptyE insert_absorb)

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
  


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


lemma event_trans_DetL: ‹P ↝e P' ⟹ P □ Q ↝e P'›
  by (metis AfterExt_Det_is_AfterExt_Ndet Un_iff τ_trans_NdetL τ_trans_event_trans ready_set_Det)
 
lemma event_trans_DetR: ‹Q ↝e Q' ⟹ P □ Q ↝e Q'›
  by (metis Det_commute event_trans_DetL)

lemma event_trans_MultiDet:
  ‹finite A ⟹ a ∈ A ⟹ P a ↝e Q ⟹ (❙□a ∈ A. P a) ↝e Q›
  by (metis MultiDet_insert' event_trans_DetL insert_absorb)


 
lemma Sliding_event_transL: ‹P ↝e P' ⟹ P ⊳ Q ↝e P'›
  unfolding Sliding_def
  apply (drule event_trans_DetL[of e P P' Q])
  using τ_trans_NdetL τ_trans_event_trans by blast


lemma Sliding_τ_transR: ‹P ⊳ Q ↝⇩τ Q›
  unfolding Sliding_def by (simp add: τ_trans_NdetR)



lemma ‹∃P P' Q. P ↝✓ P' ∧ ¬ P ❙; Q ↝✓ P' ❙; Q›
proof (intro exI)
  show ‹SKIP ↝✓ STOP ∧ ¬ SKIP ❙; STOP ↝✓ STOP ❙; STOP›
    by (simp add: SKIP_Seq SKIP_trans_tick STOP_cant_event_trans)
qed



lemma ev_trans_SeqR:
  ‹✓ ∈ ready_set P ⟹ Q ↝(ev e) Q' ⟹ P ❙; Q ↝(ev e) Q'›
  apply (simp add: AfterExt_Seq ready_set_Seq AfterExt_BOT BOT_Seq)
  using τ_trans_NdetR τ_trans_transitivity by blast
  
 


lemma ‹SKIP ⟦S⟧ SKIP ↝✓ STOP›
  by (simp add: SKIP_trans_tick Sync_SKIP_SKIP)

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


lemma tick_trans_Hiding: ‹P \ B ↝✓ STOP› if ‹P ↝✓ P'›
proof -
  have ‹(P \ B) afterExt ✓ = STOP ⊓ (P \ B) afterExt ✓›
    by (simp add: AfterExt_def Ndet_is_BOT_iff)
  thus ‹P \ B ↝✓ STOP› 
    by (simp add: AfterExt_def BOT_τ_trans_anything τ_trans_eq
                  ready_tick_imp_ready_tick_Hiding that)
qed



text ‹The following lemma is useless since the locale mechanism forces
      \<^term>‹f› to be of type \<^typ>‹'α ⇒ 'α› while it could be \<^typ>‹'α ⇒ 'β›. 
      We will have to prove it again on each instantiation of the locale.›

lemma ‹Renaming P f ↝✓ STOP› if ‹P ↝✓ P'›
proof -
  have ‹Renaming P f afterExt ✓ = STOP ⊓ Renaming P f afterExt ✓›
    by (metis AfterExt_Sliding_is_AfterExt_Ndet STOP_Sliding)
  thus ‹Renaming P f ↝✓ STOP›
    by (simp add: that tick_eq_EvExt AfterExt_def τ_trans_eq
                  ready_set_Renaming BOT_τ_trans_anything)
qed



end

end