Theory OpSemTBis

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

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


text ‹The definition with \<^term>‹(⊑⇩F⇩D)› motivates us to try with other refinements.›

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

interpretation OpSemGeneric ‹(⇩T↝⇩τ)›
  using trans_T by unfold_locales 
                    (auto simp add: anti_mono_ready_set_T mono_AfterExt_T)

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


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


section ‹Operational Semantics Laws›

text ‹\<^const>‹SKIP› law›

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



text ‹\<^term>‹e → P› laws›

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

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

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



text ‹\<^term>‹P ⊓ Q› laws›

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

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

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



text ‹\<^term>‹μ X. f X› law›

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



text ‹\<^term>‹P □ Q› laws›

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

lemma τ_trans_MultiDet:
  ‹finite A ⟹ ∀a ∈ A. P a ⇩T↝⇩τ P' a ⟹ (❙□a ∈ A. P a) ⇩T↝⇩τ (❙□a ∈ A. P' a)›
  by (fact mono_MultiDet_T)


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

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



text ‹\<^term>‹P ❙; Q› laws›

(* lemma τ_trans_SeqL: ‹P ⇩T↝⇩τ P' ⟹ P ❙; Q ⇩T↝⇩τ P' ❙; Q›
  by simp *)

(* lemma ev_trans_SeqL: ‹P ⇩T↝(ev e) P' ⟹ P ❙; Q ⇩T↝(ev e) P' ❙; Q›
  (* by (metis (no_types, lifting) AfterExt_Seq mono_Ndet_T_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 ⇩T↝✓ P' ⟹ P ❙; Q ⇩T↝⇩τ Q›
  by (metis D_SKIP D_STOP SKIP_Seq divergence_refine_def leDT_imp_leT
            leD_STOP leD_leT_imp_leDT mono_Seq_DT_left ready_tick_imp_τ_trans_SKIP)

lemma ‹Q ⇩T↝⇩τ Q' ⟹ P ❙; Q ⇩T↝⇩τ P ❙; Q'›
  by (fact mono_Seq_T_right)


(* not in the Roscoe's because direct consequence of τ_trans_SeqR *)
lemma ‹✓ ∈ ready_set P ⟹ Q ⇩T↝(ev e) Q' ⟹ P ❙; Q ⇩T↝(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 ⇩T↝⇩τ P' ⟹ P \ B ⇩T↝⇩τ P' \ B›
  by (fact mono_Hiding_T)

lemma ev_trans_Hiding_notin:
  ‹P ⇩T↝(ev e) P' ⟹ e ∉ B ⟹ P \ B ⇩T↝(ev e) P' \ B› 
  by (metis AfterExt_def After_Hiding_T_Hiding_After_if_ready_notin mono_Hiding_T 
            event_trans_τ_trans event.simps(4) ready_notin_imp_ready_Hiding)

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

lemma ev_trans_Hiding_inside:
  ‹P ⇩T↝(ev e) P' ⟹ e ∈ B ⟹ P \ B ⇩T↝⇩τ P' \ B›
  by (metis AfterExt_def Hiding_T_Hiding_After_if_ready_inside
            mono_Hiding_T event.simps(4) trans_T)

  

text ‹\<^term>‹Renaming P f› laws›

(* lemma τ_trans_Renaming: ‹P ⇩T↝⇩τ P' ⟹ Renaming P f ⇩T↝⇩τ Renaming P' f›
  by (fact mono_Renaming_T) *)

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

(* lemma ev_trans_Renaming: ‹f a = b ⟹ P ⇩T↝(ev a) P' ⟹ Renaming P f ⇩T↝(ev b) (Renaming P' f)›
  by (metis AfterExt_def After_Renaming_T UNIV_I τ_trans_Renaming ev_elem_anteced1 
            event_trans_τ_trans event.simps(4) imageI ready_set_Renaming vimageI2) *)

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

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

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


text ‹\<^term>‹P ⟦S⟧ Q› laws›

(* lemma τ_trans_SyncL: ‹P ⇩T↝⇩τ P' ⟹ P ⟦S⟧ Q ⇩T↝⇩τ P' ⟦S⟧ Q›
  and τ_trans_SyncR: ‹Q ⇩T↝⇩τ Q' ⟹ P ⟦S⟧ Q ⇩T↝⇩τ P ⟦S⟧ Q'›
  by simp_all *)

(* lemma ev_trans_SyncL: ‹e ∉ S ⟹ P ⇩T↝(ev e) P' ⟹ P ⟦S⟧ Q ⇩T↝(ev e) P' ⟦S⟧ Q ›
  and ev_trans_SyncR: ‹e ∉ S ⟹ Q ⇩T↝(ev e) Q' ⟹ P ⟦S⟧ Q ⇩T↝(ev e) P  ⟦S⟧ Q'›
  by (simp_all add: AfterExt_Sync ready_set_Sync image_iff) *)
  
(* lemma ev_trans_SyncLR: ‹e ∈ S ⟹ P ⇩T↝(ev e) P' ⟹ Q ⇩T↝(ev e) Q' ⟹ P ⟦S⟧ Q ⇩T↝(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 ⇩T↝✓ P' ⟹ P ⟦S⟧ Q ⇩T↝⇩τ SKIP ⟦S⟧ Q›
  and tick_trans_SyncR: ‹Q ⇩T↝✓ Q' ⟹ P ⟦S⟧ Q ⇩T↝⇩τ P ⟦S⟧ SKIP›
  by (simp_all add: D_SKIP divergence_refine_def leDT_imp_leT leD_leT_imp_leDT ready_tick_imp_τ_trans_SKIP)

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

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



text ‹\<^term>‹P ⊳ Q› laws›

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

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



text ‹\<^term>‹P △ Q› laws›

lemma Interrupt_τ_trans_left: ‹P ⇩T↝⇩τ P' ⟹ P △ Q ⇩T↝⇩τ P' △ Q›
  by (simp add: mono_Interrupt_T)

lemma Interrupt_τ_trans_right: ‹Q ⇩T↝⇩τ Q' ⟹ P △ Q ⇩T↝⇩τ P △ Q'›
  by (simp add: mono_Interrupt_T)

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

lemma Interrupt_ev_trans_right: ‹Q ⇩T↝(ev e) Q' ⟹ P △ Q ⇩T↝(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 ⇩T↝⇩τ P' ⟹ P Θ a ∈ A. Q a ⇩T↝⇩τ P' Θ a ∈ A. Q a›
  by (simp add: mono_Throw_T) *)

lemma Throw_τ_trans_right: 
  ‹∀a ∈ A. Q a ⇩T↝⇩τ Q' a ⟹ P Θ a ∈ A. Q a ⇩T↝⇩τ P Θ a ∈ A. Q' a›
  by (fact mono_right_Throw_T)

(* lemma Throw_event_trans_left: 
  ‹P ⇩T↝e P' ⟹ e ∉ ev ` A ⟹ P Θ a ∈ A. Q a ⇩T↝e (P' Θ a ∈ A. Q a)›
  apply (auto simp add: AfterExt_Throw ready_set_Throw split: event.split)
  by (simp add: AfterExt_def Throw_τ_trans_left)
     (metis Throw_STOP τ_trans_eq tick_trans_iff) *)

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




lemma ‹tickFree s ⟹ ⊥ ⇩T↝⇧*s P›
  by (fact BOT_trace_trans_tickFree_anything)



section ‹Reality Checks›

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



lemma T_iff_exists_trans : ‹s ∈ 𝒯 P ⟷ (∃P'. P ⇩T↝⇧*s P')›
  by (meson T_imp_exists_trace_trans trace_trans_imp_T_if_τ_trans_imp_leT)



section ‹Other Results›

lemma trace_trans_ready_set_subset_ready_set_AfterTrace: 
  ‹P ⇩T↝⇧*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 ⇩T↝⇧*(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 ⇩T↝⇧*s Q) ⟷ s ∈ 𝒯 P ∧ P afterTrace s ⇩T↝⇩τ 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›
text ‹\begin{center}
      @{thm[mode=Rule] τ_trans_DetL} \qquad
      @{thm[mode=Rule] τ_trans_DetR}
      
      @{thm[mode=Rule] event_trans_DetL} \qquad
      @{thm[mode=Rule] event_trans_DetR}
      \end{center}›

paragraph ‹\<^const>‹Seq› rule›
text ‹\begin{center}
      @{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› rule›
text ‹\begin{center}
      @{thm[mode=Rule] tick_trans_Renaming}
      \end{center}›

paragraph ‹\<^const>‹Sync› rules›
text ‹\begin{center}
      @{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_right}

      @{thm[mode=Rule, eta_contract=false] Throw_ev_trans_right}
      \end{center}›







end