Theory AfterExt

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : Extension of the After operator
 *
 * 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 ‹Extension of the After Operator›

section‹ The AfterExt Operator ›

theory  AfterExt
  imports After
begin


subsection ‹Definition›

text ‹We just defined term‹P after e› for @{term [show_types] ‹P :: 'α process›} 
      and @{term [show_types] ‹e :: 'α›}; in other words we cannot handle term‹✓›.
      We now introduce a generalisation for @{term [show_types] ‹e :: 'α event›}.›


definition AfterExt :: ‹['α process, 'α event] ⇒ 'α process› (infixl ‹afterExt› 77)
  where ‹P afterExt e ≡ case e of ev x ⇒ P after x
                                |   ✓  ⇒ if P = ⊥ then ⊥ else STOP›


lemma not_ready_AfterExt:
  ‹e ∉ ready_set P ⟹ P afterExt e = (if P = ⊥ then ⊥ else STOP)›
  by (auto simp add: AfterExt_def After_BOT intro: not_ready_After split: event.split)

lemma ready_set_AfterExt: 
  ‹ready_set (P afterExt e) = 
   (if P = ⊥ then UNIV else if e = ✓ then {} else {a. e # [a] ∈ 𝒯 P})›
  by (simp add: AfterExt_def ready_set_After ready_set_BOT 
                ready_set_STOP T_UU front_tickFree_butlast
         split: event.split) 


subsection ‹Projections›

lemma F_AfterExt: 
  ‹ℱ (P afterExt e) = 
   (   if e = ✓ ∧ P = ⊥ then {(s, X). front_tickFree s}
     else if e ∈ ready_set P then {(tl s, X)| s X. (s, X) ∈ ℱ P ∧ s ≠ [] ∧ hd s = e}
     else {(s, X). s = []})›
  (is ‹_ = ?rhs›)
proof (unfold AfterExt_def, split event.split, intro conjI allI impI)
  show ‹e = ev x ⟹ ℱ (P after x) = ?rhs› for x
    by (simp add: F_After)
next
  show ‹e = ✓ ⟹ ℱ (if P = ⊥ then ⊥ else STOP) = ?rhs›
    by (simp add: F_UU F_STOP BOT_iff_D ready_set_def set_eq_iff)
       (metis F_T T_nonTickFree_imp_decomp append_single_T_imp_tickFree hd_append2
              hd_in_set list.discI list.sel(1) list.sel(3) tickFree_def tick_T_F)
qed


lemma D_AfterExt:
  ‹𝒟 (P afterExt e) = (  if e = ✓ ∧ P = ⊥ then {s. front_tickFree s} 
                        else {tl s| s . s ∈ 𝒟 P ∧ s ≠ [] ∧ hd s = e})›
  (is ‹_ = ?rhs›)
proof (unfold AfterExt_def, split event.split, intro conjI allI impI)
  show ‹e = ev x ⟹ 𝒟 (P after x) = ?rhs› for x
    by (simp add: D_After)
       (metis Cons_in_T_imp_elem_ready_set D_T list.exhaust_sel)
next
  show ‹e = ✓ ⟹ 𝒟 (if P = ⊥ then ⊥ else STOP) = ?rhs›
    by (simp add: D_UU D_STOP BOT_iff_D)
       (metis D_imp_front_tickFree front_tickFree_implies_tickFree hd_append2
              hd_in_set is_processT9 nonTickFree_n_frontTickFree tickFree_def)
qed


lemma T_AfterExt:
  ‹𝒯 (P afterExt e) = (  if e = ✓ ∧ P = ⊥ then {s. front_tickFree s} 
                       else insert [] {tl s| s . s ∈ 𝒯 P ∧ s ≠ [] ∧ hd s = e})›
  (is ‹_ = ?rhs›)
proof (unfold AfterExt_def, split event.split, intro conjI allI impI)
  show ‹e = ev x ⟹ 𝒯 (P after x) = ?rhs› for x
    by (simp add: T_After set_eq_iff subset_iff)
       (metis Cons_in_T_imp_elem_ready_set list.collapse
              list.distinct(1) list.sel(1, 3) mem_Collect_eq ready_set_def)
next
  show ‹e = ✓ ⟹ 𝒯 (if P = ⊥ then ⊥ else STOP) = ?rhs›
  by (simp add: T_After T_UU T_STOP subset_iff)
     (metis front_tickFree_charn hd_append2 hd_in_set
            is_processT2_TR list.sel(3) tickFree_def tl_append_if)
qed



subsection ‹Monotony›

lemma mono_AfterExt : ‹P ⊑ Q ⟹ P afterExt e ⊑ Q afterExt e›
  by (auto simp add: AfterExt_def mono_After split: event.split)

lemma mono_AfterExt_T : ‹P ⊑T Q ⟹ e ≠ ✓ ∨ P = ⊥ ∨ Q ≠ ⊥ ⟹
                         P afterExt e ⊑T Q afterExt e›
  by (auto simp add: AfterExt_def mono_After_T split: event.split)

lemma mono_AfterExt_F :
  ‹P ⊑F Q ⟹ ev e ∉ ready_set P ∨ ev e ∈ ready_set Q ⟹ 
   P afterExt ev e ⊑F Q afterExt ev e›
  by (simp add: AfterExt_def mono_After_F) 

lemma mono_AfterExt_D : ‹P ⊑D Q ⟹ P afterExt e ⊑D Q afterExt e›
  by (auto simp add: AfterExt_def mono_After_D split: event.split)
     (meson BOT_iff_D divergence_refine_def subset_iff)

lemma mono_AfterExt_FD :
  ‹P ⊑FD Q ⟹ e ∉ ready_set P ∨ e ∈ ready_set Q ⟹ 
   P afterExt e ⊑FD Q afterExt e›
  by (auto simp add: AfterExt_def mono_After_FD FD_antisym split: event.split)

lemma mono_AfterExt_DT : ‹P ⊑DT Q ⟹ P afterExt e ⊑DT Q afterExt e›
  by (auto simp add: AfterExt_def mono_After_DT split: event.split)
     (meson BOT_iff_D divergence_refine_def leDT_imp_leD subsetD)
 


subsection ‹Behaviour of @{const [source] AfterExt} with const‹STOP›, const‹SKIP› and term‹⊥››

lemma AfterExt_STOP: ‹STOP afterExt e = STOP›
  by (simp add: STOP_neq_BOT STOP_iff_T T_AfterExt ready_set_STOP T_STOP)

lemma AfterExt_is_STOP_iff:
  ‹P afterExt e = STOP ⟷ P ≠ ⊥ ∧ (∀s. e # s ∈ 𝒯 P ⟶ s = [])›
  apply (cases e; simp add: AfterExt_def After_is_STOP_iff)
  by (metis After_BOT After_is_STOP_iff STOP_neq_BOT)
     (metis STOP_neq_BOT butlast.simps(2) front_tickFree_butlast is_processT2_TR tickFree_Cons)


lemma AfterExt_SKIP: ‹SKIP afterExt e = STOP›
  by (auto simp add: SKIP_neq_BOT STOP_iff_T T_AfterExt ready_set_SKIP T_SKIP)
 
lemma AfterExt_BOT : ‹⊥ afterExt e = ⊥›
  by (force simp add: BOT_iff_D D_AfterExt D_UU)

lemma AfterExt_is_BOT_iff: ‹P afterExt e = ⊥ ⟷ [e] ∈ 𝒟 P›
  apply (cases e; simp add: AfterExt_def After_is_BOT_iff)
  using BOT_iff_D D_UU STOP_neq_BOT is_processT9_tick by fastforce
 

subsection ‹Behaviour of @{const [source] AfterExt} with Operators of session‹HOL-CSP››

text ‹Here again, we lose determinism.›

lemma AfterExt_Mprefix_is_AfterExt_Mndetprefix: 
  ‹(□a ∈ A → P a) afterExt e = (⊓a ∈ A → P a) afterExt e›
  by (simp add: AfterExt_def After_Mprefix_is_After_Mndetprefix 
                Mprefix_neq_BOT Mndetprefix_neq_BOT split: event.split)
  
lemma AfterExt_Det_is_AfterExt_Ndet: ‹P □ Q afterExt e = P ⊓ Q afterExt e›
  by (simp add: AfterExt_def After_Det_is_After_Ndet Det_is_BOT_iff Ndet_is_BOT_iff
         split: event.split)


lemma AfterExt_Ndet: 
  ‹P ⊓ Q afterExt e = (  if e ∉ ready_set P ∪ ready_set Q then STOP
                       else case e of ev x ⇒   if ev x ∈ ready_set P ∩ ready_set Q
                                              then (P afterExt ev x) ⊓ (Q afterExt ev x)
                                              else   if ev x ∈ ready_set P
                                                   then P afterExt ev x
                                                   else Q afterExt ev x
                                    | ✓ ⇒ if P = ⊥ ∨ Q = ⊥ then ⊥ else STOP)›
  by (simp add: AfterExt_def Ndet_is_BOT_iff After_Ndet ready_set_BOT split: event.split)
  
 
lemma AfterExt_Mprefix: 
  ‹(□ a ∈ A → P a) afterExt e =
   (case e of ev x ⇒ if x ∈ A then P x else STOP | ✓ ⇒ STOP)›
  by (simp add: AfterExt_def Mprefix_neq_BOT After_Mprefix split: event.split)

corollary AfterExt_prefix:
  ‹(a → P) afterExt e =
   (case e of ev x ⇒ if x = a then P else STOP | ✓ ⇒ STOP)›
  unfolding write0_def by (simp add: AfterExt_Mprefix split: event.split)


lemmas AfterExt_Det = AfterExt_Ndet[folded AfterExt_Det_is_AfterExt_Ndet]
   and AfterExt_Mndetprefix = AfterExt_Mprefix
                              [unfolded AfterExt_Mprefix_is_AfterExt_Mndetprefix]


(* TODO : move this *)
lemma Renaming_is_BOT_iff: ‹Renaming P f = ⊥ ⟷ P = ⊥›
  apply (intro iffI)
   apply (simp add: BOT_iff_D D_Renaming)
  by (simp add: Renaming_BOT)

lemma Renaming_is_STOP_iff: ‹Renaming P f = STOP ⟷ P = STOP›
  apply (intro iffI, simp_all add: Renaming_STOP)
  by (auto simp add: STOP_iff_T T_Renaming intro: Nil_elem_T)


lemma AfterExt_Renaming:
  ‹Renaming P f afterExt e =
   (if P = ⊥ then ⊥ else
    ⊓a ∈ {a. ev a ∈ ready_set P ∧ ev (f a) = e}. Renaming (P afterExt ev a) f)›
  by (simp add: AfterExt_def After_Renaming Renaming_is_BOT_iff split: event.split)



―‹Move this result in session‹HOL-CSP››
lemma Seq_is_BOT_iff: ‹P ; Q = ⊥ ⟷ P = ⊥ ∨ ([✓] ∈ 𝒯 P ∧ Q = ⊥)›
  by (auto simp add: BOT_iff_D D_Seq D_UU)


lemma AfterExt_Seq:
  ‹(P ; Q) afterExt e = 
   (     if e ∉ ready_set P ∧ e ∉ ready_set Q then STOP
    else if e ∉ ready_set Q then P afterExt e ; Q
    else if e ∉ ready_set P then if ✓ ∈ ready_set P then Q afterExt e else STOP 
    else if ✓ ∈ ready_set P then (P afterExt e ; Q) ⊓ (Q afterExt e)
    else P afterExt e ; Q)›
  by (simp add: AfterExt_def After_Seq Ndet_id Ndet_is_BOT_iff 
                Seq_is_BOT_iff ready_set_def T_UU STOP_Seq split: event.split)


theorem AfterExt_Sync: 
  ‹(P ⟦S⟧ Q) afterExt e = 
   (  if P = ⊥ ∨ Q = ⊥ then ⊥ 
    else case e of ✓ ⇒ STOP
                 | ev x ⇒   if e ∈  ready_set P ∧ e ∈ ready_set Q
                           then   if x ∈ S 
                                then P afterExt e ⟦S⟧ Q afterExt e
                                else (P afterExt e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q afterExt e)
                           else   if e ∈ ready_set P
                                then   if x ∈ S then STOP else P afterExt e ⟦S⟧ Q
                                else   if e ∈ ready_set Q
                                     then   if x ∈ S then STOP else P ⟦S⟧ Q afterExt e
                                     else STOP)›
  by (simp add: AfterExt_def After_Sync Sync_is_BOT_iff split: event.split)



lemma Hiding_FD_Hiding_AfterExt_if_ready_inside:
      ‹e ∈ B ⟹ (P \ B) ⊑FD (P afterExt ev e \ B)›
  and AfterExt_Hiding_FD_Hiding_AfterExt_if_ready_notin:
      ‹e ∉ B ⟹ (P \ B) afterExt ev e ⊑FD (P afterExt ev e \ B)›
  if ready: ‹ev e ∈ ready_set P›
  by (simp add: AfterExt_def Hiding_FD_Hiding_After_if_ready_inside that)
     (simp add: AfterExt_def After_Hiding_FD_Hiding_After_if_ready_notin that)
 


lemmas Hiding_F_Hiding_AfterExt_if_ready_inside = 
       Hiding_FD_Hiding_AfterExt_if_ready_inside[THEN leFD_imp_leF]
   and AfterExt_Hiding_F_Hiding_AfterExt_if_ready_notin = 
       AfterExt_Hiding_FD_Hiding_AfterExt_if_ready_notin[THEN leFD_imp_leF]
   and Hiding_D_Hiding_AfterExt_if_ready_inside = 
       Hiding_FD_Hiding_AfterExt_if_ready_inside[THEN leFD_imp_leD]
   and AfterExt_Hiding_D_Hiding_AfterExt_if_ready_notin = 
       AfterExt_Hiding_FD_Hiding_AfterExt_if_ready_notin[THEN leFD_imp_leD]
   and Hiding_T_Hiding_AfterExt_if_ready_inside = 
       Hiding_FD_Hiding_AfterExt_if_ready_inside[THEN leFD_imp_leF, THEN leF_imp_leT]   
   and AfterExt_Hiding_T_Hiding_AfterExt_if_ready_notin = 
       AfterExt_Hiding_FD_Hiding_AfterExt_if_ready_notin[THEN leFD_imp_leF, THEN leF_imp_leT]

corollary Hiding_DT_Hiding_AfterExt_if_ready_inside:
  ‹ev e ∈ ready_set P ⟹ e ∈ B ⟹ (P \ B) ⊑DT (P afterExt ev e \ B)›
  and AfterExt_Hiding_DT_Hiding_AfterExt_if_ready_notin: 
  ‹ev e ∈ ready_set P ⟹ e ∉ B ⟹
   (P \ B) afterExt ev e ⊑DT (P afterExt ev e \ B)›
  by (simp add: Hiding_D_Hiding_AfterExt_if_ready_inside 
                Hiding_T_Hiding_AfterExt_if_ready_inside leD_leT_imp_leDT)
     (simp add: AfterExt_Hiding_D_Hiding_AfterExt_if_ready_notin 
                AfterExt_Hiding_T_Hiding_AfterExt_if_ready_notin leD_leT_imp_leDT)




subsection ‹Behaviour of @{const [source] AfterExt} with Operators of session‹HOL-CSPM››

lemma AfterExt_MultiDet_is_AfterExt_MultiNdet:
  ‹finite A ⟹ (□ a ∈ A. P a) afterExt e = (⨅ a ∈ A. P a) afterExt e›
  by (auto simp add: AfterExt_def After_MultiDet_is_After_MultiNdet
                     MultiDet_is_BOT_iff MultiNdet_is_BOT_iff split: event.split)
 

lemma AfterExt_GlobalNdet: 
  ‹(⊓ a ∈ A. P a) afterExt e = (  if e ∉ (⋃a ∈ A. ready_set (P a)) then STOP
                                else (⊓ a ∈ {a ∈ A. e ∈ ready_set (P a)}. P a) afterExt e)›
  and AfterExt_MultiNdet: 
  ‹finite A ⟹ (⨅ a ∈ A. P a) afterExt e = 
   (  if e ∉ (⋃a ∈ A. ready_set (P a)) then STOP
    else (⨅ a ∈ {a ∈ A. e ∈ ready_set (P a)}. P a) afterExt e)›
  and AfterExt_MultiDet: 
  ‹finite A ⟹ (□ a ∈ A. P a) afterExt e = 
   (  if e ∉ (⋃a ∈ A. ready_set (P a)) then STOP
    else (⨅ a ∈ {a ∈ A. e ∈ ready_set (P a)}. P a) afterExt e)›
  by ((cases e, simp_all add: AfterExt_def, 
       auto simp add: AfterExt_def ready_set_BOT After_GlobalNdet GlobalNdet_is_BOT_iff 
                      After_MultiNdet After_MultiDet MultiDet_is_BOT_iff MultiNdet_is_BOT_iff, 
       metis UNIV_I ready_set_BOT)[1])+


(* TODO: formulate and prove for MultiSync and MultiSeq *)



subsection ‹Behaviour of @{const [source] AfterExt} with Operators of session‹HOL-CSP_OpSem››

lemma AfterExt_Sliding_is_AfterExt_Ndet:
  ‹P ⊳ Q afterExt e = P ⊓ Q afterExt e›
  by (simp add: AfterExt_def After_Sliding_is_After_Ndet Sliding_is_BOT_iff Ndet_is_BOT_iff
         split: event.split)

lemmas AfterExt_Sliding = AfterExt_Ndet[folded AfterExt_Sliding_is_AfterExt_Ndet]


lemma AfterExt_Throw:
  ‹(P Θ a ∈ A. Q a) afterExt e = 
   (  if P = ⊥ then ⊥ 
    else case e of ✓ ⇒ STOP
                 | ev x ⇒   if ev x ∈ ready_set P then if x ∈ A then Q x
                           else (P after x) Θ a ∈ A. Q a else STOP)›
  by (simp add: AfterExt_def After_Throw Throw_is_BOT_iff split: event.split)


lemma AfterExt_Interrupt:
  ‹(P △ Q) afterExt e = 
   (  if P = ⊥ ∨ Q = ⊥ then ⊥
    else case e of ✓ ⇒ STOP
                 | ev x ⇒   if ev x ∈ ready_set P ∧ ev x ∈ ready_set Q
                           then (Q after x) ⊓ (P after x △ Q)
                           else   if ev x ∈ ready_set P ∧ ev x ∉ ready_set Q
                                then P after x △ Q
                                else   if ev x ∉ ready_set P ∧ ev x ∈ ready_set Q
                                     then Q after x 
                                     else STOP)›
  by (simp add: AfterExt_def After_Interrupt Interrupt_is_BOT_iff 
                Ndet_is_BOT_iff ready_set_BOT After_is_BOT_iff D_UU split: event.split)



subsection ‹Behaviour of @{const [source] AfterExt} with Reference Processes›
 
lemma AfterExt_DF: 
  ‹DF A afterExt e =
   (case e of ev x ⇒ if x ∈ A then DF A else STOP | ✓ ⇒ STOP)›
  by (cases e) (simp_all add: AfterExt_def After_DF BOT_iff_D div_free_DF)

lemma AfterExt_DFSKIP:
  ‹DFSKIP A afterExt e =
   (case e of ev x ⇒ if x ∈ A then DFSKIP A else STOP | ✓ ⇒ STOP)›
  by (cases e) (simp_all add: AfterExt_def After_DFSKIP BOT_iff_D div_free_DFSKIP)

lemma AfterExt_RUN:
  ‹RUN A afterExt e =
   (case e of ev x ⇒ if x ∈ A then RUN A else STOP | ✓ ⇒ STOP)›
  by (cases e) (simp_all add: AfterExt_def After_RUN BOT_iff_D div_free_RUN)

lemma AfterExt_CHAOS:
  ‹CHAOS A afterExt e = 
   (case e of ev x ⇒ if x ∈ A then CHAOS A else STOP | ✓ ⇒ STOP)›
  by (cases e) (simp_all add: AfterExt_def After_CHAOS BOT_iff_D div_free_CHAOS)

lemma AfterExt_CHAOSSKIP:
  ‹CHAOSSKIP A afterExt e =
   (case e of ev x ⇒ if x ∈ A then CHAOSSKIP A else STOP | ✓ ⇒ STOP)›
  by (cases e) (simp_all add: AfterExt_def After_CHAOSSKIP BOT_iff_D div_free_CHAOSSKIP)



lemma DF_FD_AfterExt:
  ‹DF A ⊑FD P ⟹ e ∈ ready_set P ⟹ DF A ⊑FD P afterExt e›
  apply (cases e, simp add: AfterExt_def DF_FD_After)
  by (metis anti_mono_ready_set_FD event.distinct(1) image_iff ready_set_DF subsetD)

lemma DFSKIP_FD_AfterExt:
  ‹DFSKIP A ⊑FD P ⟹ ev e ∈ ready_set P ⟹ DFSKIP A ⊑FD P afterExt ev e›
  by (simp add: AfterExt_def DFSKIP_FD_After)



lemma deadlock_free_AfterExt:
  ‹deadlock_free P ⟹ deadlock_free (P afterExt e) ⟷ 
                       (if e ∈ ready_set P ∧ e ≠ ✓ then True else False)›
  by (cases e)
     (simp add: AfterExt_def deadlock_free_After, 
     simp add: AfterExt_def BOT_iff_D deadlock_free_implies_div_free non_deadlock_free_STOP)

lemma deadlock_freeSKIP_AfterExt:
  ‹deadlock_freeSKIP P ⟹ deadlock_freeSKIP (P afterExt e) ⟷ 
                          (if e ∈ ready_set P ∧ e ≠ ✓ then True else False)›
  by (cases e)
     (simp add: AfterExt_def deadlock_freeSKIP_After, 
      simp add: AfterExt_def BOT_iff_D deadlock_freeSKIP_implies_div_free non_deadlock_freeSKIP_STOP)



end