Theory Events_Ticks_CSPM_Laws

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : Results on events and ticks
 *
 * 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 ‹Results on ‹events_of› and ‹ticks_of››

(*<*)
theory Events_Ticks_CSPM_Laws
  imports CSPM_Laws
begin
  (*>*)

section ‹Events›


lemma events_of_GlobalDet :
  ‹α(□a ∈ A. P a) = (⋃a∈A. α(P a))›
  by (simp add: events_of_def T_GlobalDet)

lemma strict_events_of_GlobalDet_subset : ‹α(□a ∈ A. P a) ⊆ (⋃a∈A. α(P a))›
  by (auto simp add: strict_events_of_def GlobalDet_projs)


lemma events_of_MultiSync_subset :
  ‹α(⟦S⟧ a ∈# M. P a) ⊆ (⋃a ∈ set_mset M. α(P a))›
  by (induct M rule: induct_subset_mset_empty_single, simp_all)
    (meson Diff_subset_conv dual_order.trans events_of_Sync_subset)

lemma events_of_MultiInter :
  ‹α(||| a ∈# M. P a) = (⋃a ∈ set_mset M. α(P a))›
  by (induct M rule: induct_subset_mset_empty_single)
    (simp_all add: events_of_Inter)

lemma strict_events_of_MultiSync_subset : 
  ‹α(⟦S⟧ a ∈# M. P a) ⊆ (⋃a ∈ set_mset M. α(P a))›
  by (induct M rule: induct_subset_mset_empty_single, simp_all)
    (metis (no_types, lifting) inf_sup_aci(7) le_supI2 strict_events_of_Sync_subset sup.orderE)


lemma events_of_Throw_subset :
  ‹α(P Θ a ∈ A. Q a) ⊆ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
proof (intro subsetI)
  fix e assume ‹e ∈ α(P Θ a ∈ A. Q a)›
  then obtain s where * : ‹ev e ∈ set s› ‹s ∈ 𝒯 (P Θ a ∈ A. Q a)›
    by (simp add: events_of_def) blast
  from "*"(2) consider ‹s ∈ 𝒯 P› ‹set s ∩ ev ` A = {}›
    | t1 t2   where ‹s = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
    | t1 a t2 where ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
      ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q a)›
    by (simp add: T_Throw) blast
  thus ‹e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
  proof cases
    from "*"(1) show ‹s ∈ 𝒯 P ⟹ set s ∩ ev ` A = {} ⟹
                      e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
      by (simp add: events_of_def) blast
  next
    show ‹⟦s = t1 @ t2; t1 ∈ 𝒟 P; tF t1; set t1 ∩ ev ` A = {}; ftF t2⟧ ⟹
          e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))› for t1 t2
      by (metis "*"(1) D_T UnI1 events_of_memI is_processT7)
  next
    fix t1 a t2
    assume ** : ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P›
      ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q a)›
    from "*"(1) "**"(1) have ‹ev e ∈ set (t1 @ [ev a]) ∨ ev e ∈ set t2› by simp
    thus ‹e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
    proof (elim disjE)
      show ‹ev e ∈ set (t1 @ [ev a]) ⟹ e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
        by (metis "**"(2) UnI1 events_of_memI)
    next
      show ‹ev e ∈ set t2 ⟹ e ∈ α(P) ∪ (⋃a ∈ A ∩ α(P). α(Q a))›
        by (metis (no_types, lifting) "**"(2, 4, 5) Int_iff UN_iff UnI2
            events_of_memI list.set_intros(1) set_append)
    qed
  qed
qed

(* TODO: strict_events_of *)

lemma events_of_Interrupt : ‹α(P △ Q) = α(P) ∪ α(Q)›
  by (safe elim!: events_of_memE,
      auto simp add: events_of_def Interrupt_projs)
    (metis append_Nil is_processT1_TR tickFree_Nil)

lemma strict_events_of_Interrupt_subset : ‹α(P △ Q) ⊆ α(P) ∪ α(Q)›
  by (safe elim!:strict_events_of_memE,
      auto simp add: strict_events_of_def Interrupt_projs)
    (metis DiffI T_imp_front_tickFree is_processT7)




(* TODO: see about the generalization of that *)
(* lemma events_MultiSeq:
  ‹events_of (SEQ a ∈@ L. P a) =
   (⋃a ∈ set (take (Suc (first_elem (λa. non_terminating (P a)) L)) L). 
    events_of (P a))›
  by (subst non_terminating_MultiSeq, induct L; simp add: events_SKIP events_Seq)

lemma events_MultiSeq_subset:
  ‹events_of (SEQ a ∈@ L. P a) ⊆ (⋃a ∈ set L. events_of (P a))›
  using in_set_takeD by (subst events_MultiSeq) fastforce *)






section ‹Ticks›

lemma ticks_of_GlobalDet:
  ‹ticks_of (□a ∈ A. P a) = (⋃a∈A. ticks_of (P a))›
  by (auto simp add: ticks_of_def T_GlobalDet)

lemma strict_ticks_of_GlobalDet_subset : ‹✓s(□a ∈ A. P a) ⊆ (⋃a∈A. ✓s(P a))›
  by (auto simp add: strict_ticks_of_def GlobalDet_projs)







lemma ticks_of_MultiSync_subset :
  ‹✓s(⟦S⟧ a ∈# M. P a) ⊆ (⋃a ∈ set_mset M. ✓s(P a))›
  by (induct M rule: induct_subset_mset_empty_single, simp_all)
    (meson Diff_subset_conv dual_order.trans ticks_of_Sync_subset)

lemma strict_ticks_of_MultiSync_subset :
  ‹✓s(⟦S⟧ a ∈# M. P a) ⊆ (⋂a ∈ set_mset M. ✓s(P a))›
  by (induct M rule: induct_subset_mset_empty_single, simp_all)
    (use strict_ticks_of_Sync_subset in fastforce)




lemma ticks_Throw_subset :
  ‹✓s(P Θ a∈A. Q a) ⊆ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))›
proof (rule subsetI, elim ticks_of_memE)
  fix t r assume ‹t @ [✓(r)] ∈ 𝒯 (P Θ a∈A. Q a)›
  from ‹t @ [✓(r)] ∈ 𝒯 (P Θ a∈A. Q a)› consider ‹t @ [✓(r)] ∈ 𝒯 P›
    | t1 t2   where ‹t @ [✓(r)] = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1› ‹ftF t2›
    | t1 a t2 where ‹t @ [✓(r)] = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P› ‹a ∈ A› ‹t2 ∈ 𝒯 (Q a)›
    unfolding T_Throw by blast
  thus ‹r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))›
  proof cases
    show ‹t @ [✓(r)] ∈ 𝒯 P ⟹ r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))›
      by (simp add: ticks_of_memI)
  next
    show ‹⟦t @ [✓(r)] = t1 @ t2; t1 ∈ 𝒟 P; tF t1; ftF t2⟧
          ⟹ r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))› for t1 t2
      by (cases t2 rule: rev_cases, auto)
        (metis D_T append_assoc is_processT7 ticks_of_memI)
  next
    show ‹⟦t @ [✓(r)] = t1 @ ev a # t2; t1 @ [ev a] ∈ 𝒯 P; a ∈ A; t2 ∈ 𝒯 (Q a)⟧
          ⟹ r ∈ ✓s(P) ∪ (⋃a∈A ∩ α(P). ✓s(Q a))› for t1 a t2
      by (cases t2 rule: rev_cases, simp_all)
        (meson IntI events_of_memI in_set_conv_decomp ticks_of_memI)
  qed
qed


(* TODO: strict_ticks_of *)

lemma ticks_of_Interrupt : ‹✓s(P △ Q) = ✓s(P) ∪ ✓s(Q)›
  by (safe elim!: ticks_of_memE,
      auto simp add: ticks_of_def Interrupt_projs)
    (metis append.right_neutral last_appendR snoc_eq_iff_butlast,
      metis append_Nil is_processT1_TR tickFree_Nil)

lemma strict_ticks_of_Interrupt_subset : ‹✓s(P △ Q) ⊆ ✓s(P) ∪ ✓s(Q)›
  by (safe elim!: strict_ticks_of_memE,
      auto simp add: strict_ticks_of_def Interrupt_projs)
    (meson is_processT9,
      metis (no_types, opaque_lifting) Nil_is_append_conv append_assoc
      append_butlast_last_id butlast_snoc is_processT9 last_appendR list.distinct(1))




text ‹const‹events_of› and const‹deadlock_free››

lemma nonempty_events_of_if_deadlock_free: ‹deadlock_free P ⟹ α(P) ≠ {}›
  unfolding deadlock_free_def events_of_def failure_divergence_refine_def
    failure_refine_def divergence_refine_def 
  apply (simp add: div_free_DF, subst (asm) DF_unfold)
  apply (auto simp add: F_Mndetprefix write0_def F_Mprefix subset_iff)
  by (metis (full_types) Nil_elem_T T_F is_processT5_S7
      list.set_intros(1) rangeI snoc_eq_iff_butlast)

lemma nonempty_strict_events_of_if_deadlock_free: ‹deadlock_free P ⟹ α(P) ≠ {}›
  by (metis deadlock_free_implies_div_free events_of_is_strict_events_of_or_UNIV nonempty_events_of_if_deadlock_free)

lemma events_of_in_DF: ‹DF A ⊑FD P ⟹ α(P) ⊆ A›
  by (metis anti_mono_events_of_FD events_of_DF)


lemma nonempty_events_of_if_deadlock_freeSKIP:
  ‹deadlock_freeSKIPS P ⟹ (∃r. [✓(r)] ∈ 𝒯 P) ∨ α(P) ≠ {}›
  unfolding deadlock_freeSKIPS_def events_of_def failure_refine_def 
  apply (subst (asm) DFSKIPS_unfold)
  apply (auto simp add: F_Mndetprefix write0_def F_Mprefix subset_iff F_Ndet F_SKIPS)
  by (metis eventptick.exhaust is_processT1_TR is_processT5_S7 iso_tuple_UNIV_I list.set_intros(1) self_append_conv2)


lemma events_of_in_DFSKIP: ‹DFSKIPS A R ⊑FD P ⟹ α(P) ⊆ A›
  by (metis anti_mono_events_of_FD events_of_DFSKIPS)

lemma ‹¬ α(P) ⊆ A ⟹ ¬ DF A ⊑FD P›
  and ‹¬ α(P) ⊆ A ⟹ ¬ DFSKIPS A R ⊑FD P›
  by (metis anti_mono_events_of_FD events_of_DF)
    (metis anti_mono_events_of_FD events_of_DFSKIPS)


lemma ‹chain Y ⟹ α(⨆i. Y i) = (⋃i. α(Y i))›
  apply (simp add: events_of_def limproc_is_thelub T_LUB D_LUB)
  apply auto

(* not provable as expected *)
  oops

lemma f1 : ‹chain Y ⟹ α(⨆i. Y i) = (⋃i. α(Y i))›
  apply (simp add: strict_events_of_def limproc_is_thelub T_LUB D_LUB)
  apply auto
    (* TODO: break this smt *)
  by (smt (verit, ccfv_threshold) D_T DiffI INT_iff Inter_iff le_approx2T lim_proc_is_ub rangeI ub_rangeD)

find_theorems Lub 

lemma f2 : ‹chain Y ⟹ 𝒟 (Y i) = {} ⟹ (⋃i. α(Y i)) = α(Y i)›
  apply (auto simp add: strict_events_of_def)
  by (meson ND_F_dir2' chain_lemma)

(*<*)
end
  (*>*)