Theory OpSemFBis

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

theory  OpSemFBis
  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 ‹⇩F↝⇩τ› 50)
  where ‹P ⇩F↝⇩τ Q ≡ P ⊑⇩F Q›
 
text ‹We now instantiate the locale of \<^theory>‹HOL-CSP_OpSem.OpSemGenericBis›.›

interpretation OpSemGeneric ‹(⇩F↝⇩τ) :: 'α process ⇒ 'α process ⇒ bool› 
proof unfold_locales 
  show ‹(P :: 'α process) ⊓ Q ⇩F↝⇩τ P› for P Q by simp
next
  show ‹(P :: 'α process) ⇩F↝⇩τ Q ⟹ Q ⇩F↝⇩τ R ⟹ P ⇩F↝⇩τ R› for P Q R
    by (rule trans_F)
next
  show ‹(P :: 'α process) ⇩F↝⇩τ Q ⟹ ready_set Q ⊆ ready_set P› for P Q
    by (simp add: anti_mono_ready_set_F)
next
  show ‹(e::'α event) ∈ ready_set Q ⟹ P ⇩F↝⇩τ Q ⟹ 
        P afterExt e ⇩F↝⇩τ Q afterExt e› for e P Q
    by (auto simp add: AfterExt_def mono_After_F split: event.split)
qed
   

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


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


section ‹Operational Semantics Laws›

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

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



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

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

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

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



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

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

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

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



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

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



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

(* lemma τ_trans_DetL: ‹P ⇩F↝⇩τ P' ⟹ P □ Q ⇩F↝⇩τ P' □ Q ›
  and τ_trans_DetR: ‹Q ⇩F↝⇩τ Q' ⟹ P □ Q ⇩F↝⇩τ P  □ Q'›
  by simp_all *)

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


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

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



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

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

(* lemma ev_trans_SeqL: ‹P ⇩F↝(ev e) P' ⟹ P ❙; Q ⇩F↝(ev e) P' ❙; Q›
  apply (auto simp add: ready_set_Seq AfterExt_Seq AfterExt_BOT BOT_Seq)
  (* by (metis (no_types, lifting) AfterExt_Seq mono_Ndet_F_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 ⇩F↝✓ P' ⟹ P ❙; Q ⇩F↝⇩τ Q›
  apply (elim exE conjE, drule ready_tick_imp_τ_trans_SKIP)
  by (metis (no_types, lifting) CSP_Laws.mono_Seq_FD D_Seq SKIP_Seq divergence_refine_def 
      dual_order.refl failure_divergence_refine_def leFD_imp_leF leF_leD_imp_leFD le_sup_iff)


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

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

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

lemma ev_trans_Hiding_inside:
  ‹P ⇩F↝(ev e) P' ⟹ e ∈ B ⟹ P \ B ⇩F↝⇩τ P' \ B›
  by (metis AfterExt_def Hiding_F_Hiding_After_if_ready_inside
            mono_Hiding_F event.simps(4) trans_F)

  

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

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

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

(* lemma ev_trans_Renaming: ‹f a = b ⟹ P ⇩F↝(ev a) P' ⟹ Renaming P f ⇩F↝(ev b) (Renaming P' f)›
  apply (auto simp add: AfterExt_Renaming)
  by (metis AfterExt_def After_Renaming_F 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 ⇩F↝⇩τ P' ⟹ P ⟦a := b⟧ ⇩F↝⇩τ P' ⟦a := b⟧›
  by (fact τ_trans_Renaming) *)

lemma ‹P ⇩F↝✓ P' ⟹ P ⟦a := b⟧ ⇩F↝✓ STOP›
  using tick_trans_Renaming by blast

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


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

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

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

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

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



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

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

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



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

(* lemma Interrupt_τ_trans_left: ‹P ⇩F↝⇩τ P' ⟹ P △ Q ⇩F↝⇩τ P' △ Q›
  by (simp add: mono_Interrupt_F)

lemma Interrupt_τ_trans_right: ‹Q ⇩F↝⇩τ Q' ⟹ P △ Q ⇩F↝⇩τ P △ Q'›
  by (simp add: mono_Interrupt_F) *)

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

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

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

(* lemma Throw_event_trans_left: 
  ‹P ⇩F↝e P' ⟹ e ∉ ev ` A ⟹ P Θ a ∈ A. Q a ⇩F↝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 ⇩F↝(ev e) P' ⟹ e ∈ A ⟹ P Θ a ∈ A. Q a ⇩F↝(ev e) (Q e)›
  by (simp add: AfterExt_Throw ready_set_Throw)




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



section ‹Reality Checks›

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

lemma SKIP_trace_trans_iff :
  ‹SKIP ⇩F↝⇧*s P ⟷ s = [] ∧ P = SKIP ∨ s = [✓] ∧ P = STOP›
  by (simp add: τ_trans_imp_leF_imp_SKIP_trace_trans_iff)



lemma F_iff_exists_trans :
  ‹(s, X) ∈ ℱ P ⟷ (∃P'. (P ⇩F↝⇧*s P') ∧ X ∈ ℛ P')›
  using F_imp_exists_trace_trans trace_trans_imp_F_if_τ_trans_imp_leF by blast

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



section ‹Other Results›

lemma trace_trans_ready_set_subset_ready_set_AfterTrace: 
  ‹P ⇩F↝⇧*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 ⇩F↝⇧*(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 ⇩F↝⇧*s Q) ⟷ s ∈ 𝒯 P ∧ P afterTrace s ⇩F↝⇩τ Q›
  using T_iff_exists_trans T_imp_trace_trans_iff_AfterTrace_τ_trans by blast


lemma ‹deadlock_free P ⟷ DF UNIV ⇩F↝⇩τ P›
  by (fact deadlock_free_F)

lemma ‹deadlock_free⇩S⇩K⇩I⇩P P ⟷ DF⇩S⇩K⇩I⇩P UNIV ⇩F↝⇩τ P›
  by (simp add: deadlock_free⇩S⇩K⇩I⇩P_def)


section ‹Nicely written 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] 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_event_transL}
      
      @{thm[mode=Axiom] Sliding_τ_transR}
      \end{center}›

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