Theory AfterTraceBis

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

section‹ The AfterTrace Operator, bis›

theory  AfterTraceBis
  imports AfterExtBis "HOL-CSPM.DeadlockResults"
begin


subsection ‹Definition›

text ‹We just defined \<^term>‹P afterExt e› for \<^term>‹P› an \<^typ>‹'α process› 
      and \<^term>‹e› of type \<^typ>‹'α event›.
      Since traces of an \<^typ>‹'α process› are \<^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_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)

lemma AfterTrace_BOT : ‹⊥ afterTrace s = (if tickFree s then ⊥ else STOP)›
  by (induct s) (simp_all add: AfterExt_BOT 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 list.discI list.sel(1, 3))

lemma D_AfterTrace :
  ‹tickFree (s @ t) ⟹ s @ t ∈ 𝒟 P ⟹ t ∈ 𝒟 (P afterTrace s)›
  apply (induct s arbitrary: t rule: rev_induct, solves ‹simp›)
  by (simp add: AfterTrace_snoc D_AfterExt,
      metis list.discI list.sel(1, 3) tickFree_Cons)

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_refusal_AfterTrace:
  ‹(s, X) ∈ ℱ P ⟹ ([], X) ∈ ℱ (P afterTrace s)›
  by (simp add: F_AfterTrace)

corollary D_imp_AfterTrace_is_BOT:
  ‹tickFree s ⟹ 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 ⊑⇩F⇩D Q ⟹ s ∈ 𝒯 Q ⟹ P afterTrace s ⊑⇩F⇩D 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 ⊑⇩D⇩T Q ⟹ P afterTrace s ⊑⇩D⇩T Q afterTrace s›
  by (induct s rule: rev_induct; simp add: AfterTrace_snoc mono_AfterExt_DT)




subsection ‹Another Definition of \<^const>‹events_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_free⇩S⇩K⇩I⇩P_is_right deadlock_free_def
              deadlock_free_implies_non_terminating deadlock_free_is_deadlock_free⇩S⇩K⇩I⇩P
              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_free⇩S⇩K⇩I⇩P_AfterExt_characterization: 
  ‹deadlock_free⇩S⇩K⇩I⇩P P ⟷ 
   UNIV ∉ ℛ P ∧ (∀e ∈ ready_set P - {✓}. deadlock_free⇩S⇩K⇩I⇩P (P afterExt e))›
  (is ‹deadlock_free⇩S⇩K⇩I⇩P P ⟷ ?rhs›)
proof (intro iffI)
  show ‹deadlock_free⇩S⇩K⇩I⇩P P ⟹ ?rhs›
    by (metis Diff_iff Nil_elem_T deadlock_free⇩S⇩K⇩I⇩P_AfterExt
              deadlock_free⇩S⇩K⇩I⇩P_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_free⇩S⇩K⇩I⇩P P›
  proof (unfold deadlock_free⇩S⇩K⇩I⇩P_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} ⊆ ℱ (DF⇩S⇩K⇩I⇩P UNIV)› for e
      by (simp_all add: deadlock_free⇩S⇩K⇩I⇩P_def failure_refine_def F_AfterExt non_BOT)

    fix s X
    assume ** : ‹(s, X) ∈ ℱ P›
    show ‹(s, X) ∈ ℱ (DF⇩S⇩K⇩I⇩P UNIV)›
    proof (cases s)
      show ‹s = [] ⟹ (s, X) ∈ ℱ (DF⇩S⇩K⇩I⇩P UNIV)›
        by (subst F_DF⇩S⇩K⇩I⇩P, simp)
           (metis "*"(1) "**" UNIV_eq_I event.exhaust Refusals_iff)
    next
      fix e s'
      assume *** : ‹s = e # s'›
      show ‹(s, X) ∈ ℱ (DF⇩S⇩K⇩I⇩P 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) ∈ ℱ (DF⇩S⇩K⇩I⇩P UNIV)›
          by (subst F_DF⇩S⇩K⇩I⇩P, 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) ∈ ℱ (DF⇩S⇩K⇩I⇩P UNIV)›
          by (subst F_DF⇩S⇩K⇩I⇩P, simp)
      qed
    qed
  qed
qed



end