Theory Recovered_Laws

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff.
 *
 * This file       : Recovered laws pretty printed
 *
 * Copyright (c) 2025 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 ‹ Recovered Laws pretty printed›

(*<*)
theory  Recovered_Laws
  imports Operational_Semantics_Laws "HOL-Library.LaTeXsugar"
begin
  (*>*)


section ‹General Case›

text ‹This is the general case, working for \<^term>‹(⊑⇩F⇩D)› and \<^term>‹(⊑⇩D⇩T)›.›

context OpSemTransitionsAll begin

paragraph ‹Absorbency rules›
text ‹\begin{center}
      @{thm[mode=Rule] ev_trans_τ_trans} \qquad
      @{thm[mode=Rule] τ_trans_ev_trans}
      
      @{thm[mode=Rule] tick_trans_τ_trans} \qquad
      @{thm[mode=Rule] τ_trans_tick_trans}
      \end{center}›

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

paragraph ‹\<^term>‹e → P› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] prefix_OpSem_rules(1)}

      @{thm[mode=Rule, eta_contract=false] prefix_OpSem_rules(2)}\qquad
      @{thm[mode=Rule, eta_contract=false] prefix_OpSem_rules(3)}
      \end{center}›

paragraph ‹\<^const>‹Ndet› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] Ndet_OpSem_rules(1)} \qquad
      @{thm[mode=Axiom] Ndet_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Ndet_OpSem_rules(3)}
      \end{center}›

paragraph ‹\<^term>‹μ X. f X› rule›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] fix_point_OpSem_rule}
      \end{center}›

paragraph ‹\<^const>‹Det› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(4)}
      
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(5)} \qquad
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(6)}
      \end{center}›

paragraph ‹\<^const>‹Seq› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Seq_OpSem_rules(1)}

      @{thm[mode=Rule, eta_contract=false] Seq_OpSem_rules(2)} \qquad
      @{thm[mode=Rule, eta_contract=false] Seq_OpSem_rules(3)}
      \end{center}›

paragraph ‹\<^const>‹Hiding› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(4)}
      \end{center}›

(* paragraph ‹\<^const>‹Renaming› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] prefix_OpSem_rules}
      \end{center}› *)

paragraph ‹\<^const>‹Sync› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Sync_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Sync_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Sync_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Sync_OpSem_rules(4)}

      @{thm[mode=Rule, eta_contract=false] Sync_OpSem_rules(5)}

      @{thm[mode=Rule, eta_contract=false] Sync_OpSem_rules(6)} \qquad
      @{thm[mode=Rule, eta_contract=false] Sync_OpSem_rules(7)}
    
      @{thm[mode=Axiom] Sync_OpSem_rules(8)}
      \end{center}›

paragraph ‹\<^const>‹Sliding› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] Sliding_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Sliding_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Sliding_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Sliding_OpSem_rules(4)}
      \end{center}›

paragraph ‹\<^const>‹Interrupt› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(2)} 

      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(4)} 
      
      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(5)} \qquad
      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(6)} 
      \end{center}›

paragraph ‹\<^const>‹Throw› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Throw_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Throw_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Throw_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Throw_OpSem_rules(4)}
      \end{center}›

end

context OpSemTransitionsAllDuplicated begin

paragraph ‹\<^const>‹Renaming› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Renaming_OpSem_rules(1)}

      @{thm[mode=Rule, eta_contract=false] Renaming_OpSem_rules(2)} \qquad
      @{thm[mode=Rule, eta_contract=false] Renaming_OpSem_rules(3)}
      \end{center}›

end


section ‹Special Cases›


subsection ‹With the Refinement \<^term>‹(⊑⇩D⇩T)››

context OpSemDT begin

paragraph ‹\<^const>‹Det› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] Ndet_OpSem_rules(1)[of P Q, folded τ_trans_Det_is_τ_trans_Ndet]} \qquad
      @{thm[mode=Axiom] Ndet_OpSem_rules(2)[of P Q, folded τ_trans_Det_is_τ_trans_Ndet]}
      \end{center}›

paragraph ‹\<^const>‹Sliding› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] Ndet_OpSem_rules(1)[of P Q, folded τ_trans_Sliding_is_τ_trans_Ndet]} \qquad
      @{thm[mode=Axiom] Ndet_OpSem_rules(2)[of P Q, folded τ_trans_Sliding_is_τ_trans_Ndet]}
      \end{center}›

end


subsection ‹With the Refinement \<^term>‹(⊑⇩F)››

context OpSemF begin

paragraph ‹Absorbency rules›
text ‹\begin{center}
      @{thm[mode=Rule] ev_trans_τ_trans} \qquad
      @{thm[mode=Rule] τ_trans_ev_trans}

      @{thm[mode=Rule] tick_trans_τ_trans} \qquad
      @{thm[mode=Rule] τ_trans_tick_trans}
      \end{center}›

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

paragraph ‹\<^term>‹e → P› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] prefix_OpSem_rules(1)}

      @{thm[mode=Rule, eta_contract=false] prefix_OpSem_rules(2)}\qquad
      @{thm[mode=Rule, eta_contract=false] prefix_OpSem_rules(3)}
      \end{center}›

paragraph ‹\<^const>‹Ndet› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] Ndet_OpSem_rules(1)} \qquad
      @{thm[mode=Axiom] Ndet_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Ndet_OpSem_rules(3)}
      \end{center}›

paragraph ‹\<^term>‹μ X. f X› rule›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] fix_point_OpSem_rule}
      \end{center}›

paragraph ‹\<^const>‹Det› rules›
text ‹\begin{center} 
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(4)}

      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(5)} \qquad
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(6)}
      \end{center}›

paragraph ‹\<^const>‹Seq› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] τ_trans_SeqR}
      \end{center}›

paragraph ‹\<^const>‹Hiding› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(4)}
      \end{center}›

(* paragraph ‹\<^const>‹Renaming› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] prefix_OpSem_rules}
      \end{center}› *)

paragraph ‹\<^const>‹Sync› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] τ_trans_SKIP_SyncL} \qquad
      @{thm[mode=Rule, eta_contract=false] τ_trans_SKIP_SyncR}

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

paragraph ‹\<^const>‹Sliding› rules›
text ‹\begin{center}
      @{thm[mode=Axiom, eta_contract=false] Sliding_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Sliding_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Sliding_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Sliding_OpSem_rules(4)}
      \end{center}›

paragraph ‹\<^const>‹Interrupt› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] tick_trans_InterruptL} \qquad
      @{thm[mode=Rule, eta_contract=false] tick_trans_InterruptR} 
      \end{center}›

paragraph ‹\<^const>‹Throw› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] ev_trans_ThrowR_inside} \qquad
      @{thm[mode=Rule, eta_contract=false] tick_trans_ThrowL}
      \end{center}›

end 

context OpSemFDuplicated begin

paragraph ‹\<^const>‹Renaming› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] tick_trans_Renaming}
      \end{center}›

end


subsection ‹With the Refinement \<^term>‹(⊑⇩T)››

context OpSemT begin

paragraph ‹Absorbency rules›
text ‹\begin{center}
      @{thm[mode=Rule] ev_trans_τ_trans} \qquad
      @{thm[mode=Rule] τ_trans_ev_trans}

      @{thm[mode=Rule] tick_trans_τ_trans} \qquad
      @{thm[mode=Rule] τ_trans_tick_trans}
      \end{center}›

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

paragraph ‹\<^term>‹e → P› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] prefix_OpSem_rules(1)}

      @{thm[mode=Rule, eta_contract=false] prefix_OpSem_rules(2)}\qquad
      @{thm[mode=Rule, eta_contract=false] prefix_OpSem_rules(3)}
      \end{center}›

paragraph ‹\<^const>‹Ndet› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] Ndet_OpSem_rules(1)} \qquad
      @{thm[mode=Axiom] Ndet_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Ndet_OpSem_rules(3)}
      \end{center}›

paragraph ‹\<^term>‹μ X. f X› rule›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] fix_point_OpSem_rule}
      \end{center}›

paragraph ‹\<^const>‹Det› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(4)}
      
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(5)} \qquad
      @{thm[mode=Rule, eta_contract=false] Det_OpSem_rules(6)}
      \end{center}›

paragraph ‹\<^const>‹Seq› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] τ_trans_SeqR}
      \end{center}›

paragraph ‹\<^const>‹Hiding› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Hiding_OpSem_rules(4)}
      \end{center}›

(* paragraph ‹\<^const>‹Renaming› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] prefix_OpSem_rules}
      \end{center}› *)

paragraph ‹\<^const>‹Sync› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] τ_trans_SKIP_SyncL} \qquad
      @{thm[mode=Rule, eta_contract=false] τ_trans_SKIP_SyncR}

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

paragraph ‹\<^const>‹Sliding› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] Sliding_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Sliding_OpSem_rules(2)}

      @{thm[mode=Rule, eta_contract=false] Sliding_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Sliding_OpSem_rules(4)}
      \end{center}›

paragraph ‹\<^const>‹Interrupt› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(1)} \qquad
      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(2)} 

      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(3)} \qquad
      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(4)} 
      
      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(5)} \qquad
      @{thm[mode=Rule, eta_contract=false] Interrupt_OpSem_rules(6)} 
      \end{center}›

paragraph ‹\<^const>‹Throw› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] ev_trans_ThrowR_inside} \qquad
      @{thm[mode=Rule, eta_contract=false] tick_trans_ThrowL}
      \end{center}›


text ‹Because we only look at the traces, we actully have the following results.›

paragraph ‹\<^const>‹Det› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] Ndet_OpSem_rules(1)[of P Q, folded τ_trans_Det_is_τ_trans_Ndet]} \qquad
      @{thm[mode=Axiom] Ndet_OpSem_rules(2)[of P Q, folded τ_trans_Det_is_τ_trans_Ndet]}
      \end{center}›

paragraph ‹\<^const>‹Sliding› rules›
text ‹\begin{center}
      @{thm[mode=Axiom] Ndet_OpSem_rules(1)[of P Q, folded τ_trans_Sliding_is_τ_trans_Ndet]} \qquad
      @{thm[mode=Axiom] Ndet_OpSem_rules(2)[of P Q, folded τ_trans_Sliding_is_τ_trans_Ndet]}
      \end{center}›

end

context OpSemTDuplicated begin

paragraph ‹\<^const>‹Renaming› rules›
text ‹\begin{center}
      @{thm[mode=Rule, eta_contract=false] tick_trans_Renaming}
      \end{center}›


end



(*<*)
end 
(*>*)