Theory AfterTrace

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

section‹ The AfterTrace Operator ›

theory  AfterTrace
  imports AfterExt "HOL-CSPM.DeadlockResults"
begin


subsection ‹Definition›

text ‹We just defined termP afterExt e for @{term [show_types] P ::  process}
      and @{term [show_types] e ::  event}.
      Since a trace of a termP is just an typ event list, the following 
      inductive definition is natural.›

fun AfterTrace ::  process   trace   process (infixl afterTrace 77)
  where P afterTrace [] = P
  |     P afterTrace (e # s) = P afterExt e afterTrace s



text ‹We can also induct backward.›

lemma AfterTrace_append: P afterTrace (s @ t) = P afterTrace s afterTrace t
  apply (induct t rule: rev_induct, simp)
  apply (induct s rule: rev_induct, simp)
  by (metis AfterTrace.simps append.assoc append.right_neutral append_Cons append_Nil)

lemma AfterTrace_snoc : P afterTrace (s @ [e]) = P afterTrace s afterExt e
  by (simp add: AfterTrace_append)



text ‹We have some immediate properties.›

lemma AfterTrace_BOT :  afterTrace s = 
  by (induct s) (simp_all add: AfterExt_BOT)

lemma AfterTrace_STOP : STOP afterTrace s = STOP
  by (induct s) (simp_all add: AfterExt_STOP)

lemma AfterTrace_SKIP : SKIP afterTrace s = (if s = [] then SKIP else STOP)
  by (induct s) (simp_all add: AfterExt_SKIP AfterTrace_STOP)



subsection ‹Projections›

lemma F_AfterTrace : (s @ t, X)   P  (t, X)   (P afterTrace s)
  apply (induct s arbitrary: t rule: rev_induct, simp)
  apply (simp add: AfterTrace_snoc F_AfterExt)
  by (metis Cons_in_T_imp_elem_ready_set F_T butlast_tl front_tickFree_butlast
            is_processT2 list.distinct(1) list.sel(1, 3) tickFree_tl)

lemma D_AfterTrace : s @ t  𝒟 P  t  𝒟 (P afterTrace s)
  apply (induct s arbitrary: t rule: rev_induct, simp)
  apply (simp add: AfterTrace_snoc D_AfterExt)
  by (metis D_imp_front_tickFree butlast_tl front_tickFree_butlast
            list.distinct(1) list.sel(1, 3) tickFree_tl)

lemma T_AfterTrace : s @ t  𝒯 P  t  𝒯 (P afterTrace s)
  using F_AfterTrace T_F_spec by blast


corollary ready_set_AfterTrace :
  s @ e # t  𝒯 P  e  ready_set (P afterTrace s)
  by (metis Cons_in_T_imp_elem_ready_set T_AfterTrace)

corollary F_imp_R_AfterTrace: (s, X)   P  X   (P afterTrace s)
  by (simp add: F_AfterTrace Refusals_iff)

corollary D_imp_AfterTrace_is_BOT: s  𝒟 P  P afterTrace s = 
  by (simp add: BOT_iff_D D_AfterTrace)



subsection ‹Monotony›

lemma mono_AfterTrace : P  Q  P afterTrace s  Q afterTrace s
  by (induct s rule: rev_induct) (simp_all add: mono_AfterExt AfterTrace_snoc)

lemma mono_AfterTrace_T : 
  P T Q  s  𝒯 Q  tickFree s  P afterTrace s T Q afterTrace s
  by (induct s rule: rev_induct; simp add: AfterTrace_snoc)
     (rule mono_AfterExt_T; use is_processT3_ST in blast)

lemma mono_AfterTrace_F : 
  P F Q  s  𝒯 Q  tickFree s  P afterTrace s F Q afterTrace s
  by (induct s rule: rev_induct; simp add: AfterTrace_snoc)
     (metis event.exhaust is_processT3_ST mono_AfterExt_F ready_set_AfterTrace)

lemma mono_AfterTrace_D : P D Q  P afterTrace s D Q afterTrace s
  by (induct s rule: rev_induct) (simp_all add: mono_AfterExt_D AfterTrace_snoc)

lemma mono_AfterTrace_FD :
  P FD Q  s  𝒯 Q  P afterTrace s FD Q afterTrace s
  by (induct s rule: rev_induct; simp add: AfterTrace_snoc)
     (meson Cons_in_T_imp_elem_ready_set T_AfterTrace is_processT3_ST mono_AfterExt_FD)

lemma mono_AfterTrace_DT :
  P DT Q  P afterTrace s DT Q afterTrace s
  by (induct s rule: rev_induct; simp add: AfterTrace_snoc mono_AfterExt_DT)




subsection ‹Another Definition of constevents_of

inductive reachable_event ::  process    bool
  where ev e  ready_set P  reachable_event P e
  |     reachable_event (P after f) e  reachable_event P e


lemma events_of_iff_reachable_event: e  events_of P  reachable_event P e
proof (intro iffI)
  show reachable_event P e  e  events_of P
    apply (induct rule: reachable_event.induct;
           simp add: T_After events_of_def ready_set_def split: if_split_asm)
    by (meson list.set_intros(1)) (meson list.set_sel(2))
next
  assume e  events_of P
  then obtain s where * : s  𝒯 P ev e  set s unfolding events_of_def by blast
  thus reachable_event P e
  proof (induct s arbitrary: P)
    show P e. ev e  set []  reachable_event P e by simp
  next
    case (Cons f s)
    from Cons.prems(1) is_processT3_ST 
    have * : f  ready_set P unfolding ready_set_def by force
    from Cons.prems(2) consider f = ev e | ev e  set s by auto
    thus reachable_event P e
    proof cases
      assume f = ev e
      from *[simplified this]
      show reachable_event P e by (rule reachable_event.intros(1))
    next
      assume ev e  set s
      show reachable_event P e
      proof (cases f)
        fix f'
        assume f = ev f'
        with * Cons.prems(1) have s  𝒯 (P after f') by (force simp add: T_After)
        show reachable_event P e
          apply (rule reachable_event.intros(2))
          by (rule Cons.hyps[OF s  𝒯 (P after f') ev e  set s])
      next
        from Cons.prems(1) have f =   s = [] 
          by simp (metis butlast.simps(2) front_tickFree_butlast is_processT2_TR tickFree_Cons)
        thus f =   reachable_event P e 
          using ev e  set s by force
      qed
    qed
  qed
qed


lemma reachable_event_BOT: reachable_event  e
  by (simp add: reachable_event.intros(1) ready_set_BOT)

lemma not_reachable_event_STOP: ¬ reachable_event STOP e
  by (subst events_of_iff_reachable_event[symmetric])
     (unfold events_of_def, simp add: T_STOP)

lemma reachable_tick_SKIP: ¬ reachable_event SKIP 
  by (subst events_of_iff_reachable_event[symmetric])
     (unfold events_of_def, simp add: T_SKIP)



lemma reachable_event_iff_in_ready_set_AfterTrace:
  reachable_event P e  e  {e| e s. ev e  ready_set (P afterTrace s)}
proof - 
  have reachable_event P e  s. ev e  ready_set (P afterTrace s)
  proof (induct rule: reachable_event.induct)
    case (1 e P)
    thus ?case by (metis AfterTrace.simps(1))
  next
    case (2 P f e)
    from "2.hyps"(2) obtain s where ev e  ready_set (P after f afterTrace s) by blast
    hence ev e  ready_set (P afterTrace (ev f # s)) by (simp add: AfterExt_def)
    thus ?case by blast
  qed
  also have ev e  ready_set (P afterTrace s)  reachable_event P e for s
  proof (induct s arbitrary: P)
    show ev e  ready_set (P afterTrace [])  reachable_event P e for P
      by (simp add: reachable_event.intros(1))
  next
    fix f s P
    assume  hyp : ev e  ready_set (P afterTrace s)  reachable_event P e for P
    assume prem : ev e  ready_set (P afterTrace (f # s))
    show reachable_event P e
    proof (cases f)
      fix f'
      assume f = ev f'
      show reachable_event P e by (rule reachable_event.intros(2)[OF hyp])
                                    (use prem in simp add: AfterExt_def f = ev f')
    next
      case tick
      with prem show f =   reachable_event P e
        by (simp add: AfterExt_def reachable_event_BOT AfterTrace_STOP ready_set_STOP 
               split: if_split_asm)
    qed
  qed
  ultimately show ?thesis by blast
qed




subsection ‹Characterizations for Deadlock Freeness› 

lemma deadlock_free_AfterExt_characterization: 
  deadlock_free P  range ev   P 
                       (e  ready_set P. deadlock_free (P afterExt e))
  (is deadlock_free P  ?rhs)
proof (intro iffI)
  have range ev   P  UNIV - {}   P
    by (metis Diff_insert_absorb UNIV_eq_I event.simps(3) event_set image_iff)
  thus deadlock_free P  ?rhs
    by (metis DF_FD_AfterExt Diff_Diff_Int Diff_partition Diff_subset F_T
              deadlock_freeSKIP_is_right deadlock_free_def
              deadlock_free_implies_non_terminating deadlock_free_is_deadlock_freeSKIP
              inf_top_left is_processT5_S2a non_tickFree_tick Refusals_iff self_append_conv2)
next
  assume assm : ?rhs
  with BOT_iff_D process_charn have non_BOT : P   by (metis Refusals_iff)
  show deadlock_free P
  proof (unfold deadlock_free_F failure_refine_def, safe)
    from assm have * : range ev   P
      e  ready_set P 
       {(tl s, X) |s X. (s, X)   P  s  []  hd s = e}   (DF UNIV) for e
      by (simp_all add: deadlock_free_F failure_refine_def F_AfterExt non_BOT)

    fix s X
    assume ** : (s, X)   P
    show (s, X)   (DF UNIV)
    proof (cases s)
      show s = []  (s, X)   (DF UNIV)
        by (subst F_DF, simp)
           (metis "*"(1) "**" Refusals_iff image_subset_iff is_processT4)
    next
      fix e s'
      assume *** : s = e # s'
      with "**" Cons_in_T_imp_elem_ready_set F_T have e  ready_set P by blast
      with "*"(2)[OF this] show (s, X)   (DF UNIV)
        by (subst F_DF, simp add: subset_iff)
           (metis (no_types, lifting) "*"(1) "**" "***" CollectD Refusals_iff
                  event_set hd_append2 hd_in_set in_set_conv_decomp_first insert_iff
                  is_processT6_S2 list.sel(1) list.set_intros(1) rangeE ready_set_def)
    qed
  qed
qed


lemma deadlock_freeSKIP_AfterExt_characterization: 
  deadlock_freeSKIP P  
   UNIV   P  (e  ready_set P - {}. deadlock_freeSKIP (P afterExt e))
  (is deadlock_freeSKIP P  ?rhs)
proof (intro iffI)
  show deadlock_freeSKIP P  ?rhs
    by (metis Diff_iff Nil_elem_T deadlock_freeSKIP_AfterExt
              deadlock_freeSKIP_is_right insertI1 Refusals_iff tickFree_Nil)
next
  assume assm : ?rhs
  with BOT_iff_D process_charn have non_BOT : P   by (metis Refusals_iff)
  show deadlock_freeSKIP P
  proof (unfold deadlock_freeSKIP_def failure_refine_def, safe)
    from assm have * : UNIV   P
      e  ready_set P  e   
       {(tl s, X) |s X. (s, X)   P  s  []  hd s = e}   (DFSKIP UNIV) for e
      by (simp_all add: deadlock_freeSKIP_def failure_refine_def F_AfterExt non_BOT)

    fix s X
    assume ** : (s, X)   P
    show (s, X)   (DFSKIP UNIV)
    proof (cases s)
      show s = []  (s, X)   (DFSKIP UNIV)
        by (subst F_DFSKIP, simp)
           (metis "*"(1) "**" UNIV_eq_I event.exhaust Refusals_iff)
    next
      fix e s'
      assume *** : s = e # s'
      show (s, X)   (DFSKIP UNIV)
      proof (cases e)
        fix e'
        assume e = ev e'
        with "**" "***" Cons_in_T_imp_elem_ready_set F_T
        have e  ready_set P  e   by blast
        with "*"(2)[OF this] show (s, X)   (DFSKIP UNIV)
          by (subst F_DFSKIP, simp add: subset_iff)
             (metis "**" "***" e = ev e' list.distinct(1) list.sel(1))
      next
        assume e = 
        hence s = []
          by (metis "**" "***" F_T append_butlast_last_id append_single_T_imp_tickFree
                    butlast.simps(2) list.distinct(1) tickFree_Cons)
        thus (s, X)   (DFSKIP UNIV)
          by (subst F_DFSKIP, simp)
      qed
    qed
  qed
qed



end