Theory Motivations

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : Motivations for our future definitions
 *
 * 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 ‹ Motivations for our Definitions ›

theory  Motivations
  imports AfterExt
begin


(*<*)
definition dummy_τ_trans :: ‹'α process ⇒ 'α process ⇒ bool› (infixl ‹↝τ› 50)
  where ‹P ↝τ P' ≡ undefined›

definition dummy_ev_trans :: ‹'α process ⇒ 'α event ⇒ 'α process ⇒ bool› 
                             (‹_ ↝_/ _› [50, 3, 51] 50)
  where ‹P ↝ e P' ≡ undefined›
(*>*)


text ‹To construct our bridge between denotational and operational semantics, we
      want to define two kind of transitions:  
      ▪ without external event: term‹P ↝τ P'›
      ▪ with an external event term‹e› (which can possibly be term‹✓›): term‹P ↝e P'›.

 
      We will discuss in this theory some fundamental properties that we want
     
      term‹P ↝τ Q› and term‹P ↝e Q› to verify, and on the consequences that this will have.›



text ‹Let's say we want to define the ‹τ› transition as an inductive
      predicate with three introduction rules:
      ▪ we allow a process to make a ‹τ› transition towards itself: term‹P ↝τ P›
      ▪ the non-deterministic choice const‹Ndet› can make a ‹τ› transition to the 
        left side term‹P ⊓ Q ↝τ P›
      ▪ the non-deterministic choice const‹Ndet› can make a ‹τ› transition to the
        right side term‹P ⊓ Q ↝τ Q›.›

(*<*)
no_notation dummy_τ_trans (infixl ‹↝τ› 50)
(*>*)

inductive τ_trans :: ‹'α process ⇒ 'α process ⇒ bool› (infixl ‹↝τ› 50)
  where τ_trans_eq    : ‹P ↝τ P›
  |     τ_trans_NdetL : ‹P ⊓ Q ↝τ P›
  |     τ_trans_NdetR : ‹P ⊓ Q ↝τ Q›

―‹We can obtain the same inductive predicate by removing 
   ‹τ_trans_eq› and ‹τ_trans_NdetR› clauses (because of const‹Ndet› properties).›


text ‹With this definition, we immediately show that the ‹τ›
      transition is the FD-refinement term‹(⊑FD)›.›

lemma τ_trans_is_FD: ‹(↝τ) = (⊑FD)›
  apply (intro ext iffI)
  by (metis mono_Ndet_FD_left Ndet_commute τ_trans.simps idem_FD)
     (metis mono_Ndet_FD mono_Ndet_FD_right 
            FD_antisym Ndet_id τ_trans_NdetL idem_FD)



text ‹The definition of the event transition will be a little bit more complex.

      First of all we want to prevent a process @{term [show_types] ‹P::'α process›} to make a
      transition with @{term [show_types] ‹e::'α event›} if term‹P› can not begin with term‹e›.

      More formally, we want term‹P ↝e P' ⟹ e ∈ ready_set P›.

      Moreover, we want the event transitions to absorb the ‹τ› transitions.
      
      Finally, when term‹e ∈ ready_set P›, we want to have term‹P ↝e (P afterExt e)›.
    
      This brings us to the following inductive definition:›

(*<*)
no_notation dummy_ev_trans (‹_ ↝_/ _› [50, 3, 51] 50)
(*>*)

inductive event_trans_prem :: ‹'α process ⇒ 'α event ⇒ 'α process ⇒ bool›
  where  
    τ_left_absorb : ‹⟦e ∈ ready_set P'; P ↝τ P'; event_trans_prem P' e P''⟧
                     ⟹ event_trans_prem P e P''›
  | τ_right_absorb : ‹⟦e ∈ ready_set P; event_trans_prem P e P'; P' ↝τ P''⟧
                      ⟹ event_trans_prem P e P''›
  | ready_trans_to_AfterExt : ‹e ∈ ready_set P
                              ⟹ event_trans_prem P e (P afterExt e)›

abbreviation event_trans :: ‹'α process ⇒ 'α event ⇒ 'α process ⇒ bool› 
             (‹_ ↝_/ _› [50, 3, 51] 50)
  where ‹P ↝e P' ≡ e ∈ ready_set P ∧ event_trans_prem P e P'›



text ‹We immediately show that this event transition definition is equivalent to the following:›

lemma startable_imp_ev_trans_is_startable_and_FD_After: 
  ‹(P ↝e P') ⟷ e ∈ ready_set P ∧ P afterExt e ↝τ P'›
proof safe
  show ‹e ∈ ready_set P ⟹ event_trans_prem P e P' ⟹ P afterExt e ↝τ P'›
    apply (rotate_tac, induct rule: event_trans_prem.induct)
      apply (metis τ_trans_is_FD mono_AfterExt_FD trans_FD)
     apply (metis τ_trans_is_FD trans_FD)
    by (simp add: τ_trans_is_FD)
next
  show ‹e ∈ ready_set P ⟹ P afterExt e ↝τ P' ⟹ event_trans_prem P e P'›
    by (rule τ_right_absorb[of e P ‹P afterExt e› P'])
       (simp_all add: ready_trans_to_AfterExt τ_trans_is_FD)
qed



text ‹With these two results, we are encouraged in the following theories to define:
      ▪ term‹P ↝τ Q ≡ P ⊑FD Q›
      ▪ term‹P ↝e Q ≡ e ∈ ready_set P ∧ P afterExt e ↝τ Q›


      and possible variations with other refinements.›



end