Theory OpSemFDBis

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

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


text ‹As announced in the motivations, the first definition we want to try is with term(⊑FD).›

abbreviation τ_trans ::  process   process  bool (infixl FDτ 50)
  where P FDτ Q  P FD Q
 
text ‹We now instantiate the locale of theoryHOL-CSP_OpSem.OpSemGenericBis.›

interpretation OpSemGeneric (FDτ)
  using trans_FD by unfold_locales 
                    (auto simp add: anti_mono_ready_set_FD mono_AfterExt_FD)

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


lemma P FD e P'  P' FDτ P''  P FD e P''
      P FDτ P'  P' FD e P''  P FD e P''
  by (fact event_trans_τ_trans τ_trans_event_trans)+


section ‹Operational Semantics Laws›

text constSKIP law›

lemma SKIP FD STOP
  by (fact SKIP_trans_tick)



text terme  P laws›

lemma e  A  a  A  P a FD(ev e) (P e)
  by (fact ev_trans_Mprefix)

lemma e  A  a  A  P a FD(ev e) (P e)
  by (fact ev_trans_Mndetprefix)

lemma e  P FD (ev e) P 
  by (fact ev_trans_prefix)



text termP  Q laws›

lemma P  Q FDτ P
  and P  Q FDτ Q
  by (fact τ_trans_NdetL τ_trans_NdetR)+

lemma a  A  (a  A. P a) FDτ P a
  by (fact τ_trans_GlobalNdet)

lemma finite A  a  A  (a  A. P a) FDτ P a
  by (fact τ_trans_MultiNdet)



text termμ X. f X law›

lemma cont f  P = (μ X. f X)  P FDτ f P
  by (fact fix_point_τ_trans)



text termP  Q laws›

lemma τ_trans_DetL: P FDτ P'  P  Q FDτ P'  Q
  and τ_trans_DetR: Q FDτ Q'  P  Q FDτ P   Q'
  by simp_all

lemma τ_trans_MultiDet:
  finite A  a  A. P a FDτ P' a 
   (a  A. P a) FDτ (a  A. P' a)
  by (fact mono_MultiDet_FD)


lemma P FDe P'  P  Q FDe P'
  and Q FDe Q'  P  Q FDe Q'
  by (fact event_trans_DetL event_trans_DetR)+

lemma finite A  a  A  P a FDe Q  (a  A. P a) FDe Q
  by (fact event_trans_MultiDet)



text termP ; Q laws›

lemma τ_trans_SeqL: P FDτ P'  P ; Q FDτ P' ; Q
  by simp

lemma ev_trans_SeqL: P FD(ev e) P'  P ; Q FD(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 FD P'  P ; Q FDτ 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 FD(ev e) Q'  P ; Q FD(ev e) Q'
  (* using τ_trans_SeqR τ_trans_eq τ_trans_event_trans by blast *)
  by (fact ev_trans_SeqR)



text termP \ B laws›

lemma τ_trans_Hiding: P FDτ P'  P \ B FDτ P' \ B
  by (fact mono_Hiding_FD)

lemma ev_trans_Hiding_notin:
  P FD(ev e) P'  e  B  P \ B FD(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 FD P'  P \ B FD STOP
  by (fact tick_trans_Hiding)

lemma ev_trans_Hiding_inside:
  P FD(ev e) P'  e  B  P \ B FDτ P' \ B
  by (metis AfterExt_def Hiding_FD_Hiding_After_if_ready_inside
            mono_Hiding_FD event.simps(4) trans_FD)

  

text termRenaming P f laws›

lemma τ_trans_Renaming: P FDτ P'  Renaming P f FDτ Renaming P' f
  by (fact mono_Renaming_FD)

lemma tick_trans_Renaming: P FD P'  Renaming P f FD STOP
  by (simp add: AfterExt_def ready_set_Renaming tick_eq_EvExt)

lemma ev_trans_Renaming:
  f a = b  P FD(ev a) P'  Renaming P f FD(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 FDτ P'  P a := b FDτ P' a := b
  by (fact τ_trans_Renaming)

lemma P FD P'  P a := b FD STOP
  by (fact tick_trans_Renaming)

lemma ev_trans_RenamingF:
  P FD(ev a) P'  P a := b FD(ev b) P' a := b
  by (metis ev_trans_Renaming fun_upd_same)
  


text termP S Q laws›

lemma τ_trans_SyncL: P FDτ P'  P S Q FDτ P' S Q
  and τ_trans_SyncR: Q FDτ Q'  P S Q FDτ P S Q'
  by simp_all

lemma ev_trans_SyncL:
  e  S  P FD(ev e) P'  P S Q FD(ev e) P' S Q
  and ev_trans_SyncR:
  e  S  Q FD(ev e) Q'  P S Q FD(ev e) P  S Q'
  by (simp_all add: AfterExt_Sync ready_set_Sync image_iff)
  
lemma ev_trans_SyncLR:
  e  S; P FD(ev e) P'; Q FD(ev e) Q' 
   P S Q FD(ev e) P' S Q'
  by (simp add: AfterExt_Sync ready_set_Sync)


text ‹From here we slightly defer from Roscoe's laws for constSync: 
      we obtain the following rules for constSKIP instead of constSTOP.›

lemma tick_trans_SyncL: P FD P'  P S Q FDτ SKIP S Q
  and tick_trans_SyncR: Q FD Q'  P S Q FDτ P S SKIP
  by (simp_all add: ready_tick_imp_τ_trans_SKIP)

lemma tick_trans_SKIP_Sync_SKIP: SKIP S SKIP FD STOP
  by (simp add: SKIP_trans_tick Sync_SKIP_SKIP)

lemma τ_trans_SKIP_Sync_SKIP: SKIP S SKIP FDτ SKIP
  by (simp add: Sync_SKIP_SKIP)



text termP  Q laws›

lemma Sliding_τ_trans_left: P FDτ P'  P  Q FDτ P'  Q
  unfolding Sliding_def by simp
 
lemma P FDe P'  P  Q FDe P'
  by (fact Sliding_event_transL)

lemma P  Q FDτ Q
  by (fact Sliding_τ_transR)



text termP  Q laws›

lemma Interrupt_τ_trans_left: P FDτ P'  P  Q FDτ P'  Q
  by (simp add: mono_Interrupt_FD)

lemma Interrupt_τ_trans_right: Q FDτ Q'  P  Q FDτ P  Q'
  by (simp add: mono_Interrupt_FD)

lemma Interrupt_ev_trans_left: 
  P FD(ev e) P'  P  Q FD(ev e) P'  Q
  by (simp add: AfterExt_def After_Interrupt Interrupt_τ_trans_left ready_set_Interrupt)

lemma Interrupt_ev_trans_right: Q FD(ev e) Q'  P  Q FD(ev e) Q'
  by (simp add: AfterExt_def After_Interrupt ready_set_Interrupt)



text termP Θ a  A. Q a laws›

lemma Throw_τ_trans_left:
  P FDτ P'  P Θ a  A. Q a FDτ P' Θ a  A. Q a
  by (simp add: mono_Throw_FD)

lemma Throw_τ_trans_right: 
  a  A. Q a FDτ Q' a  P Θ a  A. Q a FDτ P Θ a  A. Q' a
  by (simp add: mono_Throw_FD)

lemma Throw_event_trans_left: 
  P FDe P'  e  ev ` A  P Θ a  A. Q a FDe (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 FD(ev e) P'  e  A  P Θ a  A. Q a FD(ev e) (Q e)
  by (simp add: AfterExt_Throw ready_set_Throw split: event.split)




lemma tickFree s   FD*s P
  by (fact BOT_trace_trans_tickFree_anything)



section ‹Reality Checks›

lemma  STOP FD*s P  s = []  P = STOP
  by (fact STOP_trace_trans_iff)

lemma SKIP_trace_trans_iff :
  SKIP FD*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 FD*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 FD*s P')
  by (meson T_imp_exists_trace_trans leFD_imp_leF leF_imp_leT trace_trans_imp_T_if_τ_trans_imp_leT)

lemma tickFree_imp_D_iff_trace_trans_BOT:
  tickFree s  s  𝒟 P  P FD*s 
  using D_imp_trace_trans_BOT leFD_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 FD*s  else P FD*(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 FD*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 FD*(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 FD*s Q)  s  𝒯 P  P afterTrace s FDτ Q
  using T_iff_exists_trans T_imp_trace_trans_iff_AfterTrace_τ_trans by blast


lemma deadlock_free P  DF UNIV FDτ P
  by (simp add: deadlock_free_def)

lemma deadlock_freeSKIP P  DFSKIP UNIV FDτ P
  by (fact deadlock_freeSKIP_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 constSKIP rule›
text ‹\begin{center}
      @{thm[mode=Axiom] SKIP_trans_tick}
      \end{center}›

paragraph terme  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 constNdet 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 constDet 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 constSeq rules›
text ‹\begin{center}
      @{thm[mode=Rule] τ_trans_SeqL} \qquad
      @{thm[mode=Rule] ev_trans_SeqL}

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

paragraph constHiding 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 constRenaming 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 constSync 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 constSliding 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 constInterrupt 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 constThrow 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