Theory OpSemDTBis

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : Operational semantics with DT refinement bis
 *
 * 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‹ Trace Divergence Operational Semantics, bis›

theory  OpSemDTBis
  imports OpSemGenericBis "HOL-Library.LaTeXsugar"
begin


text ‹The definition with term‹(⊑FD)› motivates us to try with other refinements.›

abbreviation τ_trans :: ‹'α process ⇒ 'α process ⇒ bool› (infixl ‹DT↝τ› 50)
  where ‹P DT↝τ Q ≡ P ⊑DT Q›
 
text ‹We now instantiate the locale of theory‹HOL-CSP_OpSem.OpSemGenericBis›.›

interpretation OpSemGeneric ‹(DT↝τ)›
  using trans_DT by unfold_locales 
                    (auto simp add: anti_mono_ready_set_DT mono_AfterExt_DT)

notation event_trans (‹_/ DT↝_/ _›  [50, 3, 51] 50)
notation trace_trans (‹_/ DT↝*_/ _› [50, 3, 51] 50)


lemma ‹P DT↝ e P' ⟹ P' DT↝τ P'' ⟹ P DT↝ e P''›
      ‹P DT↝τ P' ⟹ P' DT↝ e P'' ⟹ P DT↝ e P''›
  by (fact event_trans_τ_trans τ_trans_event_trans)+


section‹Operational Semantics Laws›

text ‹const‹SKIP› law›

lemma ‹SKIP DT↝✓ STOP›
  by (fact SKIP_trans_tick)



text ‹term‹e → P› laws›

lemma ‹e ∈ A ⟹ □a ∈ A → P a DT↝(ev e) (P e)›
  by (fact ev_trans_Mprefix)

lemma ‹e ∈ A ⟹ ⊓a ∈ A → P a DT↝(ev e) (P e)›
  by (fact ev_trans_Mndetprefix)

lemma ‹e → P DT↝ (ev e) P› 
  by (fact ev_trans_prefix)



text ‹term‹P ⊓ Q› laws›

lemma ‹P ⊓ Q DT↝τ P›
  and ‹P ⊓ Q DT↝τ Q›
  by (fact τ_trans_NdetL τ_trans_NdetR)+

lemma ‹a ∈ A ⟹ (⊓a ∈ A. P a) DT↝τ P a›
  by (fact τ_trans_GlobalNdet)

lemma ‹finite A ⟹ a ∈ A ⟹ (⨅a ∈ A. P a) DT↝τ P a›
  by (fact τ_trans_MultiNdet)



text ‹term‹μ X. f X› law›

lemma ‹cont f ⟹ P = (μ X. f X) ⟹ P DT↝τ f P›
  by (fact fix_point_τ_trans)



text ‹term‹P □ Q› laws›

lemma τ_trans_DetL: ‹P DT↝τ P' ⟹ P □ Q DT↝τ P' □ Q ›
  and τ_trans_DetR: ‹Q DT↝τ Q' ⟹ P □ Q DT↝τ P  □ Q'›
  by simp_all

lemma τ_trans_MultiDet:
  ‹finite A ⟹ ∀a ∈ A. P a DT↝τ P' a ⟹
   (□a ∈ A. P a) DT↝τ (□a ∈ A. P' a)›
  by (fact mono_MultiDet_DT)


lemma ‹P DT↝e P' ⟹ P □ Q DT↝e P'›
  and ‹Q DT↝e Q' ⟹ P □ Q DT↝e Q'›
  by (fact event_trans_DetL event_trans_DetR)+

lemma ‹finite A ⟹ a ∈ A ⟹ P a DT↝e Q ⟹ (□a ∈ A. P a) DT↝e Q›
  by (fact event_trans_MultiDet)



text ‹term‹P ; Q› laws›

lemma τ_trans_SeqL: ‹P DT↝τ P' ⟹ P ; Q DT↝τ P' ; Q›
  by simp

lemma ev_trans_SeqL: ‹P DT↝(ev e) P' ⟹ P ; Q DT↝(ev e) P' ; Q›
  (* by (metis (no_types, lifting) AfterExt_Seq mono_Ndet_DT_left Diff_iff UNIV_I Un_iff 
               τ_trans_SeqL empty_iff event.distinct(1) insert_iff ready_set_Seq) *)
  by (auto simp add: ready_set_Seq AfterExt_Seq)

lemma τ_trans_SeqR: ‹∃P'. P DT↝✓ P' ⟹ P ; Q DT↝τ Q›
  by (metis mono_Seq_DT SKIP_Seq τ_trans_eq ready_tick_imp_τ_trans_SKIP)


(* not in the Roscoe's because direct consequence of τ_trans_SeqR *)
lemma ‹✓ ∈ ready_set P ⟹ Q DT↝(ev e) Q' ⟹ P ; Q DT↝(ev e) Q'›
  (* using τ_trans_SeqR τ_trans_eq τ_trans_event_trans by blast *)
  by (fact ev_trans_SeqR)



text ‹term‹P \ B› laws›

lemma τ_trans_Hiding: ‹P DT↝τ P' ⟹ P \ B DT↝τ P' \ B›
  by (fact mono_Hiding_DT)

lemma ev_trans_Hiding_notin:
  ‹P DT↝(ev e) P' ⟹ e ∉ B ⟹ P \ B DT↝(ev e) P' \ B› 
  by (metis AfterExt_def After_Hiding_DT_Hiding_After_if_ready_notin mono_Hiding_DT 
            event_trans_τ_trans event.simps(4) ready_notin_imp_ready_Hiding)

lemma ‹P DT↝✓ P' ⟹ P \ B DT↝✓ STOP›
  by (fact tick_trans_Hiding)

lemma ev_trans_Hiding_inside:
  ‹P DT↝(ev e) P' ⟹ e ∈ B ⟹ P \ B DT↝τ P' \ B›
  by (metis AfterExt_def Hiding_DT_Hiding_After_if_ready_inside
            mono_Hiding_DT event.simps(4) trans_DT)

  

text ‹term‹Renaming P f› laws›

lemma τ_trans_Renaming:
  ‹P DT↝τ P' ⟹ Renaming P f DT↝τ Renaming P' f›
  by (fact mono_Renaming_DT)

lemma tick_trans_Renaming: ‹P DT↝✓ P' ⟹ Renaming P f DT↝✓ STOP›
  by (simp add: AfterExt_def ready_set_Renaming tick_eq_EvExt)

lemma ev_trans_Renaming:
  ‹f a = b ⟹ P DT↝(ev a) P' ⟹ Renaming P f DT↝(ev b) (Renaming P' f)›
  apply (simp add: AfterExt_Renaming Renaming_BOT ready_set_BOT ready_set_Renaming)
  apply (intro conjI impI)
   apply (meson ev_elem_anteced1 imageI vimageI2)
  apply (rule τ_trans_transitivity[of _ ‹Renaming (P afterExt ev a) f›])
   apply (solves ‹rule τ_trans_GlobalNdet, simp›)
  by (simp add: τ_trans_Renaming)
  

(* variations with the RenamingF syntax *)
lemma ‹P DT↝τ P' ⟹ P ⟦a := b⟧ DT↝τ P' ⟦a := b⟧›
  by (fact τ_trans_Renaming)

lemma ‹P DT↝✓ P' ⟹ P ⟦a := b⟧ DT↝✓ STOP›
  by (fact tick_trans_Renaming)

lemma ev_trans_RenamingF:
  ‹P DT↝(ev a) P' ⟹ P ⟦a := b⟧ DT↝(ev b) P' ⟦a := b⟧›
  by (metis ev_trans_Renaming fun_upd_same)
  


text ‹term‹P ⟦S⟧ Q› laws›

lemma τ_trans_SyncL: ‹P DT↝τ P' ⟹ P ⟦S⟧ Q DT↝τ P' ⟦S⟧ Q›
  and τ_trans_SyncR: ‹Q DT↝τ Q' ⟹ P ⟦S⟧ Q DT↝τ P ⟦S⟧ Q'›
  by simp_all

lemma ev_trans_SyncL:
  ‹e ∉ S ⟹ P DT↝(ev e) P' ⟹ P ⟦S⟧ Q DT↝(ev e) P' ⟦S⟧ Q ›
  and ev_trans_SyncR:
  ‹e ∉ S ⟹ Q DT↝(ev e) Q' ⟹ P ⟦S⟧ Q DT↝(ev e) P  ⟦S⟧ Q'›
  by (simp_all add: AfterExt_Sync ready_set_Sync image_iff)
  
lemma ev_trans_SyncLR:
  ‹⟦e ∈ S; P DT↝(ev e) P'; Q DT↝(ev e) Q'⟧ ⟹ 
   P ⟦S⟧ Q DT↝(ev e) P' ⟦S⟧ Q'›
  by (simp add: AfterExt_Sync ready_set_Sync)


text ‹From here we slightly defer from Roscoe's laws for const‹Sync›: 
      we obtain the following rules for const‹SKIP› instead of const‹STOP›.›

lemma tick_trans_SyncL: ‹P DT↝✓ P' ⟹ P ⟦S⟧ Q DT↝τ SKIP ⟦S⟧ Q›
  and tick_trans_SyncR: ‹Q DT↝✓ Q' ⟹ P ⟦S⟧ Q DT↝τ P ⟦S⟧ SKIP›
  by (simp_all add: ready_tick_imp_τ_trans_SKIP)

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

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



text ‹term‹P ⊳ Q› laws›

lemma Sliding_τ_trans_left: ‹P DT↝τ P' ⟹ P ⊳ Q DT↝τ P' ⊳ Q›
  unfolding Sliding_def by simp
 
lemma ‹P DT↝e P' ⟹ P ⊳ Q DT↝e P'›
  by (fact Sliding_event_transL)

lemma ‹P ⊳ Q DT↝τ Q›
  by (fact Sliding_τ_transR)



text ‹term‹P △ Q› laws›

lemma Interrupt_τ_trans_left: ‹P DT↝τ P' ⟹ P △ Q DT↝τ P' △ Q›
  by (simp add: mono_Interrupt_DT)

lemma Interrupt_τ_trans_right: ‹Q DT↝τ Q' ⟹ P △ Q DT↝τ P △ Q'›
  by (simp add: mono_Interrupt_DT)

lemma Interrupt_ev_trans_left:
  ‹P DT↝(ev e) P' ⟹ P △ Q DT↝(ev e) P' △ Q›
  by (simp add: AfterExt_def After_Interrupt Interrupt_τ_trans_left ready_set_Interrupt)

lemma Interrupt_ev_trans_right: ‹Q DT↝(ev e) Q' ⟹ P △ Q DT↝(ev e) Q'›
  by (simp add: AfterExt_def After_Interrupt ready_set_Interrupt)



text ‹term‹P Θ a ∈ A. Q a› laws›

lemma Throw_τ_trans_left:
  ‹P DT↝τ P' ⟹ P Θ a ∈ A. Q a DT↝τ P' Θ a ∈ A. Q a›
  by (simp add: mono_Throw_DT)

lemma Throw_τ_trans_right: 
  ‹∀a ∈ A. Q a DT↝τ Q' a ⟹ P Θ a ∈ A. Q a DT↝τ P Θ a ∈ A. Q' a›
  by (simp add: mono_Throw_DT)

lemma Throw_event_trans_left: 
  ‹P DT↝e P' ⟹ e ∉ ev ` A ⟹ P Θ a ∈ A. Q a DT↝e (P' Θ a ∈ A. Q a)›
  apply (simp add: AfterExt_Throw ready_set_Throw image_iff split: event.split)
  apply (intro conjI impI)
  by (metis AfterExt_def Throw_τ_trans_left event.simps(4))
     (solves ‹simp add: Throw_STOP tick_trans_iff›)
 

lemma Throw_ev_trans_right: 
  ‹P DT↝(ev e) P' ⟹ e ∈ A ⟹ P Θ a ∈ A. Q a DT↝(ev e) (Q e)›
  by (simp add: AfterExt_Throw ready_set_Throw split: event.split)




lemma ‹tickFree s ⟹ ⊥ DT↝*s P›
  by (fact BOT_trace_trans_tickFree_anything)



section‹Reality Checks›

lemma  ‹STOP DT↝*s P ⟷ s = [] ∧ P = STOP›
  by (fact STOP_trace_trans_iff)





lemma T_iff_exists_trans : ‹s ∈ 𝒯 P ⟷ (∃P'. P DT↝*s P')›
  using T_imp_exists_trace_trans leDT_imp_leT trace_trans_imp_T_if_τ_trans_imp_leT by blast

lemma tickFree_imp_D_iff_trace_trans_BOT:
  ‹tickFree s ⟹ s ∈ 𝒟 P ⟷ P DT↝*s ⊥›
  using D_imp_trace_trans_BOT leDT_imp_leD trace_trans_BOT_imp_D_if_τ_trans_imp_leD by blast

lemma D_iff_trace_trans_BOT:
  ‹s ∈ 𝒟 P ⟷ (if tickFree s then P DT↝*s ⊥ else P DT↝*(butlast s) ⊥)›
  by (metis tickFree_if_trans_trans_not_STOP STOP_neq_BOT
            append_butlast_last_id front_tickFree_butlast 
            front_tickFree_single is_processT tickFree_butlast
            tickFree_imp_D_iff_trace_trans_BOT)



section‹Other Results›

lemma trace_trans_ready_set_subset_ready_set_AfterTrace: 
  ‹P DT↝*s Q ⟹ ready_set Q ⊆ ready_set (P afterTrace s)›
  by (metis T_iff_exists_trans T_imp_trace_trans_iff_AfterTrace_τ_trans τ_trans_anti_mono_ready_set)
       
lemma trace_trans_imp_ready_set:
  ‹P DT↝*(s @ e # t) Q ⟹ e ∈ ready_set (P afterTrace s)›
  using T_iff_exists_trans ready_set_AfterTrace by blast

lemma AfterTrace_τ_trans_if_τ_trans_imp_leT : 
  ‹(P DT↝*s Q) ⟷ s ∈ 𝒯 P ∧ P afterTrace s DT↝τ Q›
  using T_iff_exists_trans T_imp_trace_trans_iff_AfterTrace_τ_trans by blast


section ‹Summary: Operational Rules›

text ‹In this section, we will just write down the operational 
      laws that we have proven in a fancy way.›

paragraph ‹Absorbance rules›
text ‹\begin{center}
      @{thm[mode=Rule] event_trans_τ_trans} \qquad
      @{thm[mode=Rule] τ_trans_event_trans}
      \end{center}›

paragraph ‹const‹SKIP› rule›
text ‹\begin{center}
      @{thm[mode=Axiom] SKIP_trans_tick}
      \end{center}›

paragraph ‹term‹e → P› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] ev_trans_Mprefix} \qquad
      @{thm[mode=Rule, eta_contract=false] ev_trans_Mndetprefix}

      @{thm[mode=Axiom] ev_trans_prefix}
      \end{center}›

paragraph ‹const‹Ndet› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] τ_trans_NdetL} \qquad
      @{thm[mode=Axiom] τ_trans_NdetR}
      
      @{thm[mode=Rule, eta_contract=false] τ_trans_GlobalNdet}
      \end{center}›

paragraph ‹term‹μ X. f X› rule›
text ‹\begin{center}
      @{thm[mode=Rule] fix_point_τ_trans}
      \end{center}›

paragraph ‹const‹Det› rules (more powerful than in OpSemFD)›
text ‹\begin{center}
      @{thm[mode=Rule] τ_trans_DetL} \qquad
      @{thm[mode=Rule] τ_trans_DetR}
      \end{center}›

paragraph ‹const‹Seq› rules›
text ‹\begin{center}
      @{thm[mode=Rule] τ_trans_SeqL} \qquad
      @{thm[mode=Rule] ev_trans_SeqL}

      @{thm[mode=Rule] τ_trans_SeqR}
      \end{center}› 

paragraph ‹const‹Hiding› rules›
text ‹\begin{center}
      @{thm[mode=Rule] τ_trans_Hiding} \qquad
      @{thm[mode=Rule] tick_trans_Hiding}
      
      @{thm[mode=Rule] ev_trans_Hiding_notin} \qquad
      @{thm[mode=Rule] ev_trans_Hiding_inside}
      \end{center}›

paragraph ‹const‹Renaming› rules›
text ‹\begin{center}
      @{thm[mode=Rule] τ_trans_Renaming} \qquad
      @{thm[mode=Rule] tick_trans_Renaming}
      
      @{thm[mode=Rule] ev_trans_Renaming}
      \end{center}›

paragraph ‹const‹Sync› rules›
text ‹\begin{center}
      @{thm[mode=Rule] τ_trans_SyncL} \qquad
      @{thm[mode=Rule] τ_trans_SyncR}
      
      @{thm[mode=Rule] ev_trans_SyncL} \qquad
      @{thm[mode=Rule] ev_trans_SyncR}

      @{thm[mode=Rule] ev_trans_SyncLR}

      @{thm[mode=Rule] tick_trans_SyncL} \qquad
      @{thm[mode=Rule] tick_trans_SyncR}

      @{thm[mode=Axiom] τ_trans_SKIP_Sync_SKIP}
      \end{center}›

paragraph ‹const‹Sliding› rules›
text ‹\begin{center}
      @{thm[mode=Rule] Sliding_τ_trans_left} \qquad
      @{thm[mode=Rule] Sliding_event_transL}
      
      @{thm[mode=Axiom] Sliding_τ_transR}
      \end{center}›

paragraph ‹const‹Interrupt› rules›
text ‹\begin{center}
      @{thm[mode=Rule] Interrupt_τ_trans_left} \qquad
      @{thm[mode=Rule] Interrupt_τ_trans_right}
      
      @{thm[mode=Rule] Interrupt_ev_trans_left} \qquad
      @{thm[mode=Rule] Interrupt_ev_trans_right}
      \end{center}›

paragraph ‹const‹Throw› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Throw_τ_trans_left} \qquad
      @{thm[mode=Rule, eta_contract=false] Throw_τ_trans_right}
      
      @{thm[mode=Rule, eta_contract=false] Throw_event_trans_left} \qquad
      @{thm[mode=Rule, eta_contract=false] Throw_ev_trans_right}
      \end{center}›






end