Theory AfterExtBis

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

theory  AfterExtBis
  imports After
begin

section ‹The AfterExt Operator, bis›


subsection ‹Definition›

text ‹The refinements \<^term>‹(⊑⇩F)› and \<^term>‹(⊑⇩T)› are not verifying the locale axioms.
      In order to make the constructions available for these refinements, we
      will slightly modify the definition of AfterExt.›

text ‹If the event is \<^term>‹✓› we obtain \<^const>‹STOP›
      anyway, even if the process was \<^term>‹⊥›. 

      At first this appears a little weird, but can be interpreted as the fact
      that even if a process if diverging, after accepting \<^term>‹✓› it has to stop.›

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


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

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


subsection ‹Projections›

lemma F_AfterExt: 
  ‹ℱ (P afterExt e) = 
   (   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 = ✓ ⟹ ℱ 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 {} 
                                        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 = ✓ ⟹ 𝒟 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 {[]} 
                                       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 = ✓ ⟹ 𝒯 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 ⟹ 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 (simp add: AfterExt_def mono_After_D split: event.split)

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

lemma mono_AfterExt_DT : ‹P ⊑⇩D⇩T Q ⟹ P afterExt e ⊑⇩D⇩T Q afterExt e›
  by (simp add: AfterExt_def mono_After_DT split: event.split)
 


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 = ⊥ ∧ e = ✓ ∨ (∀s. e # s ∈ 𝒯 P ⟶ s = [])›
  by (simp add: AfterExt_def After_is_STOP_iff split: event.split)
     (metis T_nonTickFree_imp_decomp append_single_T_imp_tickFree 
            butlast.simps(2) butlast_snoc 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 = (if e = ✓ then STOP else ⊥)›
  by (metis AfterExt_def After_BOT event.case event.exhaust)

lemma AfterExt_is_BOT_iff: ‹P afterExt e = ⊥ ⟷ e ≠ ✓ ∧ [e] ∈ 𝒟 P›
  by (simp add: AfterExt_def After_is_BOT_iff STOP_neq_BOT split: event.split)
 
 

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 = ( 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
                                | ✓ ⇒ STOP)›
  by (auto simp add: AfterExt_def After_Ndet not_ready_After 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 =
   (case e of ✓ ⇒ STOP 
            | ev a ⇒ 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 = 
   (  case e of ✓ ⇒ STOP
                 | ev x ⇒   if P = ⊥ ∨ Q = ⊥ then ⊥  
                           else 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 split: event.split)
  



lemma Hiding_FD_Hiding_AfterExt_if_ready_inside:
  ‹e ∈ B ⟹ (P \ B) ⊑⇩F⇩D (P afterExt ev e \ B)›
  and AfterExt_Hiding_FD_Hiding_AfterExt_if_ready_notin:
  ‹e ∉ B ⟹ (P \ B) afterExt ev e ⊑⇩F⇩D (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) ⊑⇩D⇩T (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 ⊑⇩D⇩T (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 = ✓ ∨ 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 = ✓ ∨ 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 = ✓ ∨ e ∉ (⋃a ∈ A. ready_set (P a)) then STOP
    else (⨅ a ∈ {a ∈ A. e ∈ ready_set (P a)}. P a) afterExt e)›
  by (simp_all add: AfterExt_def split: event.split)
     (simp add: After_GlobalNdet, simp add: After_MultiNdet, simp add: After_MultiDet)


(* 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 = 
   (case e of ✓ ⇒ STOP
            | ev x ⇒   if P = ⊥ then ⊥ 
                      else    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 = 
   (case e of ✓ ⇒ STOP
            | ev x ⇒   if P = ⊥ ∨ Q = ⊥ then ⊥
                      else   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_DF⇩S⇩K⇩I⇩P:
  ‹DF⇩S⇩K⇩I⇩P A afterExt e =
   (case e of ev x ⇒ if x ∈ A then DF⇩S⇩K⇩I⇩P A else STOP | ✓ ⇒ STOP)›
  by (cases e) (simp_all add: AfterExt_def After_DF⇩S⇩K⇩I⇩P BOT_iff_D div_free_DF⇩S⇩K⇩I⇩P)

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_CHAOS⇩S⇩K⇩I⇩P:
  ‹CHAOS⇩S⇩K⇩I⇩P A afterExt e =
   (case e of ev x ⇒ if x ∈ A then CHAOS⇩S⇩K⇩I⇩P A else STOP | ✓ ⇒ STOP)›
  by (cases e) (simp_all add: AfterExt_def After_CHAOS⇩S⇩K⇩I⇩P BOT_iff_D div_free_CHAOS⇩S⇩K⇩I⇩P)



lemma DF_FD_AfterExt:
  ‹DF A ⊑⇩F⇩D P ⟹ e ∈ ready_set P ⟹ DF A ⊑⇩F⇩D 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 DF⇩S⇩K⇩I⇩P_FD_AfterExt:
  ‹DF⇩S⇩K⇩I⇩P A ⊑⇩F⇩D P ⟹ ev e ∈ ready_set P ⟹ DF⇩S⇩K⇩I⇩P A ⊑⇩F⇩D P afterExt ev e›
  by (simp add: AfterExt_def DF⇩S⇩K⇩I⇩P_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_free⇩S⇩K⇩I⇩P_AfterExt:
  ‹deadlock_free⇩S⇩K⇩I⇩P P ⟹ deadlock_free⇩S⇩K⇩I⇩P (P afterExt e) ⟷ 
                          (if e ∈ ready_set P ∧ e ≠ ✓ then True else False)›
  by (cases e)
     (simp add: AfterExt_def deadlock_free⇩S⇩K⇩I⇩P_After, 
      simp add: AfterExt_def BOT_iff_D deadlock_free⇩S⇩K⇩I⇩P_implies_div_free non_deadlock_free⇩S⇩K⇩I⇩P_STOP)



end