Theory EventsProperties

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

theory EventsProperties
  imports CSPM
begin



section ‹With Operators of \<^session>‹HOL-CSP››

lemma events_of_def_tickFree: 
  ‹events_of P = (⋃t∈{t ∈ 𝒯 P. tickFree t}. {a. ev a ∈ set t})›
proof -
  have ‹s ∈ 𝒯 P ⟹ ¬ tickFree s ⟹ ev e ∈ set s ⟹ ev e ∈ set (butlast s)› for e s
    by (cases s rule: rev_cases) (simp_all add: append_single_T_imp_tickFree)
  thus ?thesis
    by (auto simp add: events_of_def)
       (metis butlast_snoc front_tickFree_butlast is_processT2_TR
              is_processT3_ST nonTickFree_n_frontTickFree)
qed


lemma events_BOT:  ‹events_of ⊥ = UNIV›
  and events_SKIP: ‹events_of SKIP = {}›
  and events_STOP: ‹events_of STOP = {}›
  by (auto simp add: events_of_def T_UU T_SKIP T_STOP)
     (meson front_tickFree_single list.set_intros(1))


lemma anti_mono_events_T: ‹P ⊑⇩T Q ⟹ events_of Q ⊆ events_of P›
  unfolding trace_refine_def events_of_def by fast

lemma anti_mono_events_F: ‹P ⊑⇩F Q ⟹ events_of Q ⊆ events_of P›
  by (intro anti_mono_events_T leF_imp_leT)

lemma anti_mono_events_FD: ‹P ⊑⇩F⇩D Q ⟹ events_of Q ⊆ events_of P›
  by (intro anti_mono_events_F leFD_imp_leF)



lemmas events_fix_prefix = 
       events_DF[of ‹{a}›, simplified DF_def Mndetprefix_unit] for a

lemma events_Mndetprefix:
  ‹events_of (Mndetprefix A P) = A ∪ (⋃a∈A. events_of (P a))›
  apply (cases ‹A = {}›, simp add: events_STOP)
  unfolding events_of_def 
  apply (simp add: T_Mndetprefix T_Mprefix write0_def, safe; simp)
    apply (metis event.inject list.exhaust_sel set_ConsD)
  by (metis Nil_elem_T list.sel(1, 3) list.set_intros(1)) 
     (metis list.sel(1, 3) list.set_intros(2))


lemma events_Mprefix:
  ‹events_of (Mprefix A P) = A ∪ (⋃a∈A. events_of (P a))›
  apply (rule subset_antisym)
   apply (rule subset_trans[OF anti_mono_events_FD[OF Mprefix_refines_Mndetprefix_FD]],
          simp add: events_Mndetprefix)
  unfolding events_of_def 
  apply (simp add: T_Mprefix, safe; simp)
  by (metis Nil_elem_T list.sel(1, 3) list.set_intros(1))
     (metis list.sel(1, 3) list.set_intros(2))


lemma events_prefix: ‹events_of (a → P) = insert a (events_of P)›
  unfolding write0_def by (simp add: events_Mprefix)


lemma events_Ndet: ‹events_of (P ⊓ Q) = events_of P ∪ events_of Q›
  unfolding events_of_def by (simp add: T_Ndet)


lemma events_Det: ‹events_of (P □ Q) = events_of P ∪ events_of Q›
  unfolding events_of_def by (simp add: T_Det)


lemma events_Renaming:
  ‹events_of (Renaming P f) = (if 𝒟 P = {} then f ` events_of P else UNIV)›
proof (split if_split, intro conjI impI)
  show ‹𝒟 P ≠ {} ⟹ events_of (Renaming P f) = UNIV›
    by (rule events_div, simp add: D_Renaming)
       (metis D_imp_front_tickFree ex_in_conv front_tickFree_charn
        front_tickFree_implies_tickFree is_processT9_S_swap nonTickFree_n_frontTickFree)
next
  show ‹events_of (Renaming P f) = f ` events_of P› if div_free : ‹𝒟 P = {}›
  proof (intro subset_antisym subsetI)
    fix e
    assume ‹e ∈ events_of (Renaming P f)›
    then obtain s t where * : ‹t ∈ 𝒯 P› ‹s = map (EvExt f) t› ‹ev e ∈ set s›
      by (auto simp add: events_of_def T_Renaming div_free)
    from "*"(2, 3) obtain e' where ‹e = f e'› ‹ev e' ∈ set t›
      by (auto simp add: EvExt_def split: event.split_asm)
    with "*"(1) show ‹e ∈ f ` events_of P›
      unfolding events_of_def by blast
  next
    fix e
    assume ‹e ∈ f ` events_of P›
    then obtain e' where * : ‹e = f e'› ‹e' ∈ events_of P› by blast
    from "*"(2) obtain t where ‹t ∈ 𝒯 P› ‹ev e' ∈ set t›
      unfolding events_of_def by blast
    thus ‹e ∈ events_of (Renaming P f)›
      apply (simp add: events_of_def T_Renaming)
      apply (rule disjI1)
      apply (rule_tac x = ‹map (EvExt f) t› in exI)
      using "*"(1) by (auto simp add: EvExt_def image_iff split: event.split)
  qed
qed
     
     


lemma events_Seq:
  ‹events_of (P ❙; Q) =
   (if non_terminating P then events_of P else events_of P ∪ events_of Q)›
proof (split if_split, intro conjI impI)
  show ‹non_terminating P ⟹ events_of (P ❙; Q) = events_of P›
    by (simp add: non_terminating_Seq)
next
  show ‹events_of (P ❙; Q) = events_of P ∪ events_of Q› if ‹¬ non_terminating P›
  proof (intro subset_antisym subsetI)
    show ‹e ∈ events_of (P ❙; Q) ⟹ e ∈ events_of P ∪ events_of Q› for e
      by (auto simp add: events_of_def T_Seq F_T D_T intro: is_processT3_ST)
  next
    fix s
    assume ‹s ∈ events_of P ∪ events_of Q›
    then consider ‹s ∈ events_of P› | ‹s ∈ events_of Q› by fast
    thus ‹s ∈ events_of (P ❙; Q)›
    proof cases
      show ‹s ∈ events_of P ⟹ s ∈ events_of (P ❙; Q)›
        by (simp add: events_of_def_tickFree T_Seq)
           (metis Nil_elem_T append.right_neutral is_processT5_S7 singletonD)
    next
      from non_terminating_refine_DF that 
      obtain t1 where * : ‹t1 ∈ 𝒯 P› ‹t1 ∉ 𝒯 (DF UNIV)›
        by (metis subsetI trace_refine_def)
      then obtain t1' where ‹t1 = t1' @ [tick]›
        using DF_all_tickfree_traces2 T_nonTickFree_imp_decomp is_processT3_ST by blast
      hence ‹t2 ∈ 𝒯 Q ⟹ t1' @ t2 ∈ 𝒯 (P ❙; Q)› for t2
        using "*"(1) T_Seq by blast
      thus ‹s ∈ events_of Q ⟹ s ∈ events_of (P ❙; Q)›
        by (simp add: events_of_def, elim bexE)
           (metis UnCI set_append)
    qed
  qed
qed



lemma events_Sync: ‹events_of (P ⟦S⟧ Q) ⊆ events_of P ∪ events_of Q›
  apply (subst events_of_def, subst T_Sync, simp add: subset_iff)
proof (intro allI impI conjI, goal_cases)
  case (1 a)
  thus ?case by (metis (no_types, lifting) UN_I events_of_def ftf_Sync1 mem_Collect_eq) 
next
  case (2 a)
  then obtain t u where ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P› by blast
  thus ?case using events_div by blast
qed


lemma events_Inter:
  ‹events_of ((P :: 'α process) ||| Q) = events_of P ∪ events_of Q›
proof (rule subset_antisym[OF events_Sync])
  have ‹⟦tickFree s; s ∈ 𝒯 (P :: 'α process)⟧ ⟹ s ∈ 𝒯 (P ||| Q)› for s P Q
    apply (simp add: T_Sync)
    apply (rule disjI1)
    apply (rule_tac x = s in exI, simp)
    apply (rule_tac x = ‹[]› in exI, simp add: Nil_elem_T)
    by (metis Sync.sym emptyLeftSelf singletonD tickFree_def)
  hence ‹events_of (P :: 'α process) ⊆ events_of (P ||| Q)› for P Q
    unfolding events_of_def_tickFree by fast
  thus ‹events_of P ∪ events_of Q ⊆ events_of (P ||| Q)›
    by (metis Inter_commute Un_least)
qed



lemma empty_div_hide_events_Hiding: ‹events_of (P \ B) ⊆ events_of P - B›
  if ‹div_hide P B = {}›
  unfolding events_of_def T_Hiding
  apply (subst that, simp)
  using F_T by auto blast

lemma not_empty_div_hide_events_Hiding:
  ‹div_hide P B ≠ {} ⟹ events_of (P \ B) = UNIV›
  using D_Hiding events_div by blast



text ‹\<^const>‹events_of› and \<^const>‹deadlock_free››

lemma nonempty_events_if_deadlock_free: ‹deadlock_free P ⟹ events_of P ≠ {}›
  unfolding deadlock_free_def events_of_def failure_divergence_refine_def le_ref_def 
  apply (simp add: div_free_DF, subst (asm) DF_unfold)
  apply (simp add: F_Mndetprefix write0_def F_Mprefix subset_iff)
  by (metis Nil_elem_T T_F_spec UNIV_I hd_in_set is_processT5_S7
            list.distinct(1) self_append_conv2)

lemma events_in_DF: ‹DF A ⊑⇩F⇩D P ⟹ events_of P ⊆ A›
  by (metis anti_mono_events_FD events_DF)


lemma nonempty_events_if_deadlock_free⇩S⇩K⇩I⇩P:
  ‹deadlock_free⇩S⇩K⇩I⇩P P ⟹ [tick] ∈ 𝒯 P ∨ events_of P ≠ {}›
  unfolding deadlock_free⇩S⇩K⇩I⇩P_def events_of_def failure_refine_def le_ref_def 
  apply (subst (asm) DF⇩S⇩K⇩I⇩P_unfold)
  apply (simp add: F_Mndetprefix write0_def F_Mprefix subset_iff F_Ndet F_SKIP)
  by (metis Nil_elem_T T_F_spec UNIV_I hd_in_set is_processT5_S7
            list.distinct(1) self_append_conv2)

lemma events_in_DF⇩S⇩K⇩I⇩P: ‹DF⇩S⇩K⇩I⇩P A ⊑⇩F⇩D P ⟹ events_of P ⊆ A›
  by (metis anti_mono_events_FD events_DF⇩S⇩K⇩I⇩P)

lemma ‹¬ events_of P ⊆ A ⟹ ¬ DF A ⊑⇩F⇩D P›
  and ‹¬ events_of P ⊆ A ⟹ ¬ DF⇩S⇩K⇩I⇩P A ⊑⇩F⇩D P›
  by (metis anti_mono_events_FD events_DF)
     (metis anti_mono_events_FD events_DF⇩S⇩K⇩I⇩P)
  
 

section ‹With Architectural Operators of \<^session>‹HOL-CSPM››

lemma events_MultiNdet:
  ‹finite A ⟹ events_of (MultiNdet A P) = (⋃a∈A. events_of (P a))›
  by (cases ‹A = {}›, simp add: events_STOP)
     (rotate_tac, induct A rule: finite_set_induct_nonempty; simp add: events_Ndet)
  

lemma events_MultiDet:
  ‹finite A ⟹ events_of (MultiDet A P) = (⋃a∈A. events_of (P a))›
  by (induct A rule: finite_induct) (simp_all add: events_STOP events_Det)


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



lemma events_MultiSync:
  ‹events_of (❙⟦S❙⟧ a ∈# M. P a) ⊆ (⋃a ∈ set_mset M. events_of (P a))›
  by (induct M rule: induct_subset_mset_empty_single; simp add: events_STOP)
     (meson Diff_subset_conv dual_order.trans events_Sync)


lemma events_MultiInter:
  ‹events_of (❙|❙|❙| a ∈# M. P a) = (⋃a ∈ set_mset M. events_of (P a))›
  by (induct M rule: induct_subset_mset_empty_single)
     (simp_all add: events_STOP events_Inter)
 



end