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) 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 ‹ Motivations for our Definitions ›

(*<*)
theory  Motivations
  imports After_Ext_Operator
begin
  (*>*)

(*<*)
definition dummy_τ_trans :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool› (infixl ‹↝τ› 50)
  where ‹P ↝τ P' ≡ undefined›

definition dummy_event_trans :: ‹[('a, 'r) processptick, 'a, ('a, 'r) processptick] ⇒ bool› (‹_ ↝⇘_⇙ _› [50, 3, 51] 50)
  where ‹P ↝⇘e⇙ P' ≡ undefined›

definition dummy_tick_trans :: ‹[('a, 'r) processptick, 'r, ('a, 'r) processptick] ⇒ bool› (‹_ ↝✓⇘_⇙ _› [50, 3, 51] 50)
  where ‹P ↝✓⇘r⇙ 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 the terminating event term‹✓(r)›: term‹P ↝✓⇘r⇙ P'›
      ▪ with a non terminating external event term‹ev e›: term‹P ↝⇘e⇙ P'›.

      We will discuss in this theory some fundamental properties that we want
     
      term‹P ↝τ Q›, term‹P ↝⇘e⇙ P'› and term‹P ↝✓⇘r⇙ P'› to verify, and 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 :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ 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 Ndet_FD_self_left Ndet_FD_self_right τ_trans.simps order_class.order_eq_iff)
    (metis FD_antisym Ndet_FD_self_left Ndet_id τ_trans_NdetR mono_Ndet_FD)


(*<*)
context AfterExt
begin
  (*>*)

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 :: ('a, 'r) processptick›}
      to make a transition with @{term [show_types] ‹ev e :: ('a, 'r) eventptick›}
      (resp. @{term [show_types] ‹✓(r) :: ('a, 'r) eventptick›})
      if term‹P› can not begin with term‹ev e› (resp. term‹✓(r)›).

      More formally, we want term‹P ↝⇘e⇙ P' ⟹ ev e ∈ initials P› (resp. term‹P ↝✓⇘r⇙ P' ⟹ ✓(r) ∈ P0›).

      Moreover, we want the event transitions to absorb the ‹τ› transitions.
      
      Finally, when term‹e ∈ P0› (resp. term‹✓(r) ∈ P0›), we want to have
      term‹P ↝⇘e⇙ P after✓ ev e› (resp. term‹P ↝✓⇘r⇙ P after✓ ✓(r)›).
    
      This brings us to the following inductive definition:›

(*<*)
no_notation dummy_event_trans (‹_ ↝⇘_⇙ _›  [50, 3, 51] 50)
no_notation dummy_tick_trans  (‹_ ↝✓⇘_⇙ _› [50, 3, 51] 50)
  (*>*)

inductive event_trans_prem :: ‹('a, 'r) processptick ⇒ ('a, 'r) eventptick ⇒ ('a, 'r) processptick ⇒ bool›
  where  
    τ_left_absorb : ‹⟦e ∈ initials P'; P ↝τ P'; event_trans_prem P' e P''⟧
                     ⟹ event_trans_prem P e P''›
  | τ_right_absorb : ‹⟦e ∈ initials P; event_trans_prem P e P'; P' ↝τ P''⟧
                      ⟹ event_trans_prem P e P''›
  | initial_trans_to_Aftertick : ‹e ∈ initials P ⟹ event_trans_prem P e (P after✓ e)›

abbreviation event_trans :: ‹('a, 'r) processptick ⇒ 'a ⇒ ('a, 'r) processptick ⇒ bool› 
  (‹_ ↝⇘_⇙ _› [50, 3, 51] 50)
  where ‹P ↝⇘e⇙ P' ≡ ev e ∈ initials P ∧ event_trans_prem P (ev e) P'›

abbreviation tick_trans :: ‹('a, 'r) processptick ⇒ 'r ⇒ ('a, 'r) processptick ⇒ bool› (‹_ ↝✓⇘_⇙ _› [50, 3, 51] 50)
  where ‹P ↝✓⇘r⇙ P' ≡ ✓(r) ∈ P0 ∧ event_trans_prem P ✓(r) P'›



text ‹We immediately show that, under the assumption of monotony of term‹Ω›,
      this event transition definition is equivalent to the following:›

lemma startable_imp_ev_trans_is_startable_and_FD_After: 
  ‹(case e of ev x ⇒ P ↝⇘x⇙ P' | ✓(r) ⇒ P ↝✓⇘r⇙ P') ⟷ e ∈ P0 ∧ P after✓ e ↝τ P'›
  if ‹⋀P Q. case e of ✓(r) ⇒ Ω P r ↝τ Ω Q r›
proof -
  have ‹(case e of ev x ⇒ P ↝⇘x⇙ P' | ✓(r) ⇒ P ↝✓⇘r⇙ P') ⟷
        e ∈ initials P ∧ event_trans_prem P e P'› by (simp split: eventptick.split)
  also have ‹… ⟷ e ∈ initials P ∧ P after✓ e ↝τ P'›
  proof (insert that, safe)
    show ‹event_trans_prem P e P' ⟹ e ∈ P0 ⟹
          (⋀P Q. case e of ✓(r) ⇒ Ω P r ↝τ Ω Q r) ⟹ P after✓ e ↝τ P'›
    proof (induct rule: event_trans_prem.induct)
      case (τ_left_absorb e P' P P'')
      thus ?case 
        apply (cases e)
         apply (metis (mono_tags, lifting) τ_trans_is_FD eventptick.simps(5) mono_Aftertick_FD trans_FD)
        by (metis Aftertick_def FD_antisym τ_trans_is_FD eventptick.simps(6))
    next
      case (τ_right_absorb e P P' P'')
      thus ?case by (metis τ_trans_is_FD trans_FD)
    next
      case (initial_trans_to_Aftertick e P)
      thus ?case by (simp add: τ_trans_eq)
    qed
  next
    show ‹e ∈ initials P ⟹ P after✓ e ↝τ P' ⟹ event_trans_prem P e P'›
      by (rule τ_right_absorb[of e P ‹P after✓ e› P'])
        (simp_all add: initial_trans_to_Aftertick τ_trans_is_FD)
  qed
  finally show ?thesis .
qed



text ‹With these two results, we are encouraged in the following theories to define:
       ▪ term‹P ↝τ Q ≡ P ⊑FD Q›
       ▪ term‹P ↝⇘e⇙ P' ≡ ev e ∈ initials P ∧ P after✓ (ev e) ↝τ Q›
       ▪ term‹P ↝✓⇘r⇙ P' ≡ ✓(r) ∈ P0 ∧ P after✓ ✓(r) ↝τ Q›

      and possible variations with other refinements.›

(*<*)

no_notation τ_trans (infixl ‹↝τ› 50)
no_notation event_trans (‹_ ↝⇘_⇙ _›  [50, 3, 51] 50)
no_notation tick_trans  (‹_ ↝✓⇘_⇙ _› [50, 3, 51] 50)

end 


(*>*)

text ‹But we want to make the construction as general as possible.
      Therefore we will continue with the locale mechanism, eventually adding additional required
      assumptions for each operator, and we will instantiate with refinements at the end.›


(*<*)
end
  (*>*)