Theory OpSemFD

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

theory  OpSemFD
  imports OpSemGeneric "HOL-Library.LaTeXsugar"
begin


text ‹As announced in the motivations, the first definition we want to try is with \<^term>‹(⊑⇩_F⇩_D)›.›

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

interpretation OpSemGeneric ‹(⇩_F⇩_D↝⇩_τ)›
  using trans_FD by unfold_locales 
                    (auto simp add: anti_mono_ready_set_FD mono_AfterExt_FD)

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


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


section ‹Operational Semantics Laws›

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

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



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

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

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

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



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

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

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

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



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

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



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

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

lemma τ_trans_MultiDet:
  ‹finite A ⟹ ∀a ∈ A. P a ⇩_F⇩_D↝⇩_τ P' a ⟹ 
   (❙□a ∈ A. P a) ⇩_F⇩_D↝⇩_τ (❙□a ∈ A. P' a)›
  by (fact mono_MultiDet_FD)


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

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



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

lemma τ_trans_SeqL: ‹P ⇩_F⇩_D↝⇩_τ P' ⟹ P ❙; Q ⇩_F⇩_D↝⇩_τ P' ❙; Q›
  by simp

lemma ev_trans_SeqL: ‹P ⇩_F⇩_D↝(ev e) P' ⟹ P ❙; Q ⇩_F⇩_D↝(ev e) P' ❙; Q›
  (* by (metis (no_types, lifting) AfterExt_Seq mono_Ndet_FD_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⇩_D↝✓ P' ⟹ P ❙; Q ⇩_F⇩_D↝⇩_τ Q›
  by (metis mono_Seq_FD 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 ⇩_F⇩_D↝(ev e) Q' ⟹ P ❙; Q ⇩_F⇩_D↝(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⇩_D↝⇩_τ P' ⟹ P \ B ⇩_F⇩_D↝⇩_τ P' \ B›
  by (fact mono_Hiding_FD)

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

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

lemma ev_trans_Hiding_inside:
  ‹P ⇩_F⇩_D↝(ev e) P' ⟹ e ∈ B ⟹ P \ B ⇩_F⇩_D↝⇩_τ P' \ B›
  by (metis AfterExt_def Hiding_FD_Hiding_After_if_ready_inside
            mono_Hiding_FD event.simps(4) trans_FD)

  

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

lemma τ_trans_Renaming:
  ‹P ⇩_F⇩_D↝⇩_τ P' ⟹ Renaming P f ⇩_F⇩_D↝⇩_τ Renaming P' f›
  by (fact mono_Renaming_FD)

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

lemma ev_trans_Renaming:
  ‹f a = b ⟹ P ⇩_F⇩_D↝(ev a) P' ⟹ Renaming P f ⇩_F⇩_D↝(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 ⇩_F⇩_D↝⇩_τ P' ⟹ P ⟦a := b⟧ ⇩_F⇩_D↝⇩_τ P' ⟦a := b⟧›
  by (fact τ_trans_Renaming)

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

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


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

lemma τ_trans_SyncL: ‹P ⇩_F⇩_D↝⇩_τ P' ⟹ P ⟦S⟧ Q ⇩_F⇩_D↝⇩_τ P' ⟦S⟧ Q›
  and τ_trans_SyncR: ‹Q ⇩_F⇩_D↝⇩_τ Q' ⟹ P ⟦S⟧ Q ⇩_F⇩_D↝⇩_τ P ⟦S⟧ Q'›
  by simp_all

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

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

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



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

lemma Sliding_τ_trans_left: ‹P ⇩_F⇩_D↝⇩_τ P' ⟹ P ⊳ Q ⇩_F⇩_D↝⇩_τ P' ⊳ Q›
  by (simp add: Sliding_def)
 
lemma ‹P ⇩_F⇩_D↝e P' ⟹ P ⊳ Q ⇩_F⇩_D↝e P'›
  by (fact Sliding_event_transL)

lemma ‹P ⊳ Q ⇩_F⇩_D↝⇩_τ Q›
  by (fact Sliding_τ_transR)



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

lemma Interrupt_τ_trans_left: ‹P ⇩_F⇩_D↝⇩_τ P' ⟹ P △ Q ⇩_F⇩_D↝⇩_τ P' △ Q›
  by (simp add: mono_Interrupt_FD)

lemma Interrupt_τ_trans_right: ‹Q ⇩_F⇩_D↝⇩_τ Q' ⟹ P △ Q ⇩_F⇩_D↝⇩_τ P △ Q'›
  by (simp add: mono_Interrupt_FD)

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

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

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

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





lemma ‹front_tickFree s ⟹ ⊥ ⇩_F⇩_D↝⇧^*s P›
  by (fact BOT_trace_trans_anything)



section ‹Reality Checks›

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

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



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

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

lemma D_iff_trace_trans_BOT: ‹s ∈ 𝒟 P ⟷ P ⇩_F⇩_D↝⇧^*s ⊥›
  using D_imp_trace_trans_BOT leFD_imp_leD trace_trans_BOT_imp_D_if_τ_trans_imp_leD by blast
 


section ‹Other Results›

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


lemma ‹deadlock_free P ⟷ DF UNIV ⇩_F⇩_D↝⇩_τ P›
  by (simp add: deadlock_free_def)

lemma ‹deadlock_free⇩_S⇩_K⇩_I⇩_P P ⟷ DF⇩_S⇩_K⇩_I⇩_P UNIV ⇩_F⇩_D↝⇩_τ P›
  by (fact deadlock_free⇩_S⇩_K⇩_I⇩_P_FD)


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› 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