Quelle  Initials.thy

(*<*)
―‹ ********************************************************************
 * Project : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author : Benoît Ballenghien, Burkhart Wolff.
 *
 * This file : Initials events of a process
 *
 * 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 ‹ The Initials Notion ›

(*<*)
theory  Initials
  imports "HOL-CSPM"
begin
  (*>*)


text ‹This will be discussed more precisely later, but we want to define a new operator
 which would in some way be the reciprocal of the prefix operator term‹e → P›.

 A first observation is that by prefixing term‹P› with term‹e›,
 we force its nonempty traces to begin with term‹ev e›.

 Therefore we must define a notion that captures this idea.›

section ‹Definition›

text ‹The initials notion captures the set of events that can be used to begin a given process.›

definition initials :: ‹('a, 'r) process_ptick ==> ('a, 'r) event_ptick set› (‹(_⁰)› [1000] 999)
  where ‹P⁰ ≡ {e. [e] ∈ T P}›

lemma initials_memI' : ‹[e] ∈ T P ==> e ∈ P⁰›
  and initials_memD  : ‹e ∈ P⁰ ==> [e] ∈ T P›
  by (simp_all add: initials_def)

lemma initials_def_bis: ‹P⁰ = {e. ∃s. e # s ∈ T P}›
  by (simp add: set_eq_iff initials_def)
    (metis Prefix_Order.prefixI append_Cons append_Nil is_processT3_TR)

lemma initials_memI : ‹e # s ∈ T P ==> e ∈ P⁰›
  unfolding initials_def_bis by blast


text ‹We say here that the const‹initials› of a process term‹P› is the set
 of events term‹e› such that there is a trace of term‹P› starting with term‹e›.

 One could also think about defining term‹initials P› as the set of events that
 term‹P› can not refuse at first: term‹{e. {e} ∉ R P}›.
 These two definitions are not equivalent (and the second one is more restrictive
 than the first one). Moreover, the second does not behave well with the
 non-deterministic choice const‹Ndet› (see the 🪙‹notepad› below).
 
 Therefore, we will keep the first one.

 We also have a strong argument of authority: this is the definition given
 by Roscoe cite‹‹p.40› in "Roscoe2010UnderstandingCS"›.›


notepad
begin
  fix e :: ‹('a, 'r) event_ptick› ―‹just fixing 🍋‹'a› type›

  define bad_initials
    where ‹bad_initials (P :: ('a, 'r) process_ptick) ≡ {e. {e} ∉ R P}› for P

―‹This notion is more restrictive than const‹initials››
  have bad_initials_subset_initials:
    ‹bad_initials P ⊆ initials P› for P
    unfolding bad_initials_def initials_def Refusals_iff
    using is_processT1_TR is_processT5_S7 by force

―‹and does not behave well with @{const [source] Ndet}.›
  have bad_behaviour_with_Ndet: 
    ‹∃P Q. bad_initials (P ⊓ Q) ≠ bad_initials P ∪ bad_initials Q›
  proof (intro exI)
    show ‹bad_initials (SKIP undefined ⊓ ⊥) ≠ bad_initials (SKIP undefined) ∪ bad_initials ⊥›
      by (simp add: bad_initials_def F_Ndet F_SKIP F_BOT Refusals_iff)
  qed
end



section ‹Anti-Mono Rules›

lemma anti_mono_initials_T: ‹P ⊑_T Q ==> initials Q ⊆ initials P›
  by (simp add: Collect_mono_iff trace_refine_def initials_def subsetD)

lemma anti_mono_initials_F: ‹P ⊑_F Q ==> initials Q ⊆ initials P›
  unfolding failure_refine_def
  by (drule F_subset_imp_T_subset) (fact anti_mono_initials_T[unfolded trace_refine_def])

text ‹Of course, this anti-monotony does not hold for term‹(⊑_D)›.›

lemma anti_mono_initials_FD: ‹P ⊑_FD Q ==> initials Q ⊆ initials P›
  by (simp add: anti_mono_initials_F leFD_imp_leF)

lemma anti_mono_initials: ‹P ⊑ Q ==> initials Q ⊆ initials P›
  by (simp add: anti_mono_initials_T le_approx_lemma_T trace_refine_def)

lemma anti_mono_initials_DT: ‹P ⊑_DT Q ==> initials Q ⊆ initials P›
  by (simp add: anti_mono_initials_T leDT_imp_leT)


section ‹Behaviour of const‹initials› with const‹STOP›, const‹SKIP› and term‹⊥››

lemma initials_STOP [simp] : ‹STOP⁰ = {}›
  by (simp add: initials_def T_STOP)

text ‹We already had @{thm STOP_iff_T}. As an immediate consequence we obtain a
 characterization of being const‹STOP› involving const‹initials›.›

lemma initials_empty_iff_STOP: ‹P⁰ = {} ⟷ P = STOP›
proof (intro iffI)
  { assume ‹T P ≠ {[]}›
    then obtain a s where ‹a # s ∈ T P›
      by (metis Nil_elem_T is_singleton_the_elem is_singletonI'
          list.exhaust_sel singletonI empty_iff)
    with initials_memD initials_memI have ‹∃a. [a] ∈ T P› by blast}
  thus ‹P⁰ = {} ==> P = STOP›
    by (simp add: STOP_iff_T initials_def) presburger
next
  show ‹P = STOP ==> P⁰ = {}› by simp
qed


lemma initials_SKIP [simp] : ‹(SKIP r)⁰ = {🍋(r)}›
  by (simp add: initials_def T_SKIP)

lemma initials_SKIPS [simp] : ‹(SKIPS R)⁰ = tick ` R›
  by (auto simp add: initials_def T_SKIPS)

lemma initials_BOT [simp] : ‹⊥⁰ = UNIV›
  by (simp add: initials_def T_BOT)

text ‹These two, on the other hand, are not characterizations.›

lemma ‹∃P. P⁰ = {🍋(r)} ∧ P ≠ (SKIP r)›
proof (intro exI)
  show ‹(STOP ⊓ SKIP r)⁰ = {🍋(r)} ∧ STOP ⊓ SKIP r ≠ SKIP r›
    by (simp add: initials_def T_Ndet T_STOP T_SKIP)
      (metis Ndet_FD_self_left SKIP_FD_iff SKIP_neq_STOP)
qed

lemma ‹∃P. P⁰ = UNIV ∧ P ≠ ⊥›
proof (intro exI)
  show ‹((◻a ∈ UNIV → ⊥) ⊓ SKIPS UNIV)⁰ = UNIV ∧ (◻a ∈ UNIV → ⊥) ⊓ SKIPS UNIV ≠ ⊥›
    by (simp add: set_eq_iff BOT_iff_Nil_D Ndet_projs Mprefix_projs
        SKIPS_projs initials_def) (metis event_ptick.exhaust)
qed


text ‹But when term‹🍋(r) ∈ P⁰›, we can still have this refinement:›

lemma initial_tick_iff_FD_SKIP : ‹🍋(r) ∈ P⁰ ⟷ P ⊑_FD SKIP r›
proof (intro iffI)
  show ‹🍋(r) ∈ P⁰ ==> P ⊑_FD SKIP r›
    unfolding failure_divergence_refine_def failure_refine_def divergence_refine_def
    by (simp add: F_SKIP D_SKIP subset_iff initials_def)
      (metis append_Nil is_processT6_TR_notin tick_T_F)
next
  show ‹P ⊑_FD SKIP r ==> 🍋(r) ∈ P⁰› by (auto dest: anti_mono_initials_FD)
qed


lemma initial_ticks_iff_FD_SKIPS : ‹R ≠ {} ==> tick ` R ⊆ P<sup>0</sup> ⟷ P ⊑<sub>FD</sub> SKIPS R›
proof (rule iffI)
  show ‹R ≠ {} ==> tick ` R ⊆ P⁰ ==> P ⊑_FD SKIPS R›
    by (unfold SKIPS_def, rule mono_GlobalNdet_FD_const)
      (simp_all add: image_subset_iff initial_tick_iff_FD_SKIP)
next
  show ‹P ⊑_FD SKIPS R ==> tick ` R ⊆ P⁰›
    by (metis anti_mono_initials_FD initials_SKIPS)
qed



text ‹We also obtain characterizations for term‹P ; Q = ⊥›.›

lemma Seq_is_BOT_iff : ‹P ; Q = ⊥ ⟷ P = ⊥ ∨ (∃r. 🍋(r) ∈ P⁰ ∧ Q = ⊥)›
  by (simp add: BOT_iff_Nil_D D_Seq initials_def)

(* lemma MultiSeq_is_BOT_iff:
  \<open>(SEQ l \<in>@ L. P l) = \<bottom> \<longleftrightarrow> 
   (\<exists>j < first_elem (\<lambda>l. range \<checkmark> \<inter> initials (P l) = {}) L. P (L ! j) = \<bottom>)\<close>
  apply (induct L)
  apply (solves \<open>simp add: SKIP_neq_BOT\<close>)
  using initials_BOT less_Suc_eq_0_disj by (auto simp add: Seq_is_BOT_iff) *)



section ‹Behaviour of const‹initials› with Operators of session‹HOL-CSP››

lemma initials_Mprefix :     ‹(◻a ∈ A → P a)⁰ = ev ` A›
  and initials_Mndetprefix : ‹(⊓a ∈ A → P a)<sup>0</sup> = ev ` A›
  and initials_write0 :      ‹(a → Q)⁰ = {ev a}›
  and initials_write :       ‹(c!a → Q)⁰ = {ev (c a)}›
  and initials_read :        ‹(c?a∈A → P a)⁰ = ev ` c ` A›
  and initials_ndet_write :  ‹(c!!a∈A → P a)⁰ = ev ` c ` A›
  by (auto simp: initials_def T_Mndetprefix write0_def
      write_def T_Mprefix read_def ndet_write_def)


text ‹As discussed earlier, const‹initials› behaves very well
 with term‹(◻)›, term‹(⊓)› and term‹(⊳)›.›

lemma initials_Det :     ‹(P ◻ Q)⁰ = P⁰ ∪ Q⁰›
  and initials_Ndet :    ‹(P ⊓ Q)⁰ = P⁰ ∪ Q⁰›
  and initials_Sliding : ‹(P ⊳ Q)⁰ = P⁰ ∪ Q⁰›
  by (auto simp add: initials_def T_Det T_Ndet T_Sliding)


lemma initials_Seq: 
  ‹(P ; Q)⁰ = ( if P = ⊥ then UNIV
 else P⁰ - range tick ∪ (∪r∈{r. 🍋(r) ∈ P⁰}. Q⁰))›
  (is ‹_ = (if _ then _ else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹P = ⊥ ==> (P ; Q)⁰ = UNIV› by simp
next
  show ‹(P ; Q)⁰ = P⁰ - range tick ∪ (∪r∈{r. 🍋(r) ∈ P⁰}. Q⁰)› if ‹P ≠ ⊥›
  proof (intro subset_antisym subsetI)
    fix e assume ‹e ∈ (P ; Q)⁰›
    from event_ptick.exhaust consider a where ‹e = ev a› | r where ‹e = 🍋(r)› by blast
    thus ‹e ∈ ?rhs›
    proof cases
      from ‹e ∈ (P ; Q)⁰› show ‹e = ev a ==> e ∈ ?rhs› for a
        by (simp add: image_iff initials_def T_Seq)
          (metis (no_types, lifting) D_T append_Cons append_Nil
            is_processT3_TR_append list.exhaust_sel list.sel(1))
    next
      from ‹e ∈ (P ; Q)⁰› ‹P ≠ ⊥› show ‹e = 🍋(r) ==> e ∈ ?rhs› for r
        by (simp add: image_iff initials_def T_Seq BOT_iff_tick_D)
          (metis (no_types, opaque_lifting) append_T_imp_tickFree append_eq_Cons_conv
            event_ptick.disc(2) not_Cons_self2 tickFree_Cons_iff)
    qed
  next
    fix e assume ‹e ∈ ?rhs›
    then consider a where ‹e = ev a› ‹ev a ∈ P⁰›
      | r where ‹🍋(r) ∈ P⁰› ‹e ∈ Q⁰›
      by simp (metis empty_iff event_ptick.exhaust rangeI)
    thus ‹e ∈ (P ; Q)⁰›
    proof cases
      show ‹e = ev a ==> ev a ∈ P⁰ ==> e ∈ (P ; Q)⁰› for a
        by (simp add: initials_def T_Seq)
    next
      show ‹🍋(r) ∈ P⁰ ==> e ∈ Q⁰ ==> e ∈ (P ; Q)⁰› for r
        by (simp add: initials_def T_Seq) (metis append_Nil)
    qed
  qed
qed




lemma initials_Sync:
  ‹(P [S] Q)⁰ = (if P = ⊥ ∨ Q = ⊥ then UNIV else
 P⁰ ∪ Q⁰ - (range tick ∪ ev ` S) ∪ P<sup>0</sup> ∩ Q<sup>0</sup> ∩ (range tick ∪ ev ` S))›
  (is ‹(P [S] Q)⁰ = (if P = ⊥ ∨ Q = ⊥ then UNIV else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹P = ⊥ ∨ Q = ⊥ ==> (P [S] Q)⁰ = UNIV›
    by (metis Sync_is_BOT_iff initials_BOT)
next
  show ‹(P [S] Q)⁰ = ?rhs› if non_BOT : ‹¬ (P = ⊥ ∨ Q = ⊥)›
  proof (intro subset_antisym subsetI)
    show ‹e ∈ ?rhs ==> e ∈ (P [S] Q)⁰› for e
    proof (elim UnE)
      assume ‹e ∈ P⁰ ∪ Q⁰ - (range tick ∪ ev ` S)›
      hence ‹[e] ∈ T P ∨ [e] ∈ T Q› ‹e ∉ range tick ∪ ev ` S›
        by (auto dest: initials_memD)
      have ‹[e] setinterleaves (([e], []), range tick ∪ ev ` S)›
        using ‹e ∉ range tick ∪ ev ` S› by simp
      with ‹[e] ∈ T P ∨ [e] ∈ T Q› is_processT1_TR setinterleaving_sym
      have ‹[e] ∈ T (P [S] Q)› by (simp (no_asm) add: T_Sync) blast
      thus ‹e ∈ (P [S] Q)⁰› by (simp add: initials_memI)
    next
      assume ‹e ∈ P⁰ ∩ Q⁰ ∩ (range tick ∪ ev ` S)›
      hence ‹[e] ∈ T P› ‹[e] ∈ T Q› ‹e ∈ range tick ∪ ev ` S›
        by (simp_all add: initials_memD)
      have ‹[e] setinterleaves (([e], [e]), range tick ∪ ev ` S)›
        using ‹e ∈ range tick ∪ ev ` S› by simp
      with ‹[e] ∈ T P› ‹[e] ∈ T Q› have ‹[e] ∈ T (P [S] Q)›
        by (simp (no_asm) add: T_Sync) blast
      thus ‹e ∈ (P [S] Q)⁰› by (simp add: initials_memI)
    qed
  next
    fix e
    assume ‹e ∈ (P [S] Q)⁰›
    then consider t u where ‹t ∈ T P› ‹u ∈ T Q› ‹[e] setinterleaves ((t, u), range tick ∪ ev ` S)›
      | (div) t u r v where ‹ftF v› ‹tF r ∨ v = []› ‹[e] = r @ v›
        ‹r setinterleaves ((t, u), range tick ∪ ev ` S)›
        ‹t ∈ D P ∧ u ∈ T Q ∨ t ∈ D Q ∧ u ∈ T P›
      by (simp add: initials_def T_Sync) blast
    thus ‹e ∈ ?rhs›
    proof cases
      show ‹t ∈ T P ==> u ∈ T Q ==> [e] setinterleaves ((t, u), range tick ∪ ev ` S)
 ==> e ∈ ?rhs› for t u
        by (cases t; cases u; simp add: initials_def image_iff split: if_split_asm)
          (use empty_setinterleaving setinterleaving_sym in blast)+
    next
      case div
      have ‹r ≠ []› using div(4, 5) BOT_iff_Nil_D empty_setinterleaving that by blast
      hence ‹r = [e] ∧ v = []›
        by (metis (no_types, lifting) div(3) Nil_is_append_conv append_eq_Cons_conv)
      also from div(5) BOT_iff_Nil_D non_BOT
      obtain e' t' where ‹t = e' # t'› by (cases t) blast+
      ultimately show ‹e ∈ ?rhs›
        using div(4, 5)
        by (cases u, simp_all add: initials_def subset_iff T_Sync image_iff split: if_split_asm)
          (metis [[metis_verbose = false]] D_T setinterleaving_sym empty_setinterleaving)+
    qed
  qed
qed



lemma initials_Renaming:
  ‹(Renaming P f g)⁰ = (if P = ⊥ then UNIV else map_event_ptick f g ` P<sup>0</sup>)›
proof (split if_split, intro conjI impI)
  show ‹P = ⊥ ==> (Renaming P f g)<sup>0</sup> = UNIV› by simp
next
  assume ‹P ≠ ⊥›
  hence ‹[] ∉ D P› by (simp add: BOT_iff_Nil_D)
  show ‹(Renaming P f g)<sup>0</sup> = map_event<sub>ptick</sub> f g ` P⁰›
  proof (intro subset_antisym subsetI)
    fix e assume ‹e ∈ (Renaming P f g)⁰›
    with ‹[] ∉ D P› obtain s where * : ‹[e] = map (map_event_ptick f g) s› ‹s ∈ T P›
      by (simp add: initials_def T_Renaming)
        (metis D_T append.right_neutral append_is_Nil_conv list.map_disc_iff list.sel(3) tl_append2)
    from "*"(1) obtain e' where ** : ‹s = [e']› ‹e = map_event_ptick f g e'› by blast
    from "**"(1) "*"(2) have ‹e' ∈ P⁰› by (simp add: initials_def)
    with "**"(2) show ‹e ∈ map_event_ptick f g ` P<sup>0</sup>› by simp
  next
    fix e assume ‹e ∈ map_event<sub>ptick</sub> f g ` P⁰›
    then obtain e' where ‹e = map_event_ptick f g e'› ‹e' ∈ P⁰› by fast
    thus ‹e ∈ (Renaming P f g)⁰› by (auto simp add: initials_def T_Renaming)
  qed
qed




text ‹Because for the expression of its traces (and more specifically of its divergences),
 dealing with const‹Hiding› is much more difficult.›

text ‹We start with two characterizations:
 ▪ the first one to understand prop‹P \ S = ⊥›
 ▪ the other one to understand prop‹[e] ∈ D (P \ S)›.›

lemma Hiding_is_BOT_iff : 
  ‹P \ S = ⊥ ⟷ (∃t. set t ⊆ ev ` S ∧
 (t ∈ D P ∨ (∃ f. isInfHiddenRun f P S ∧ t ∈ range f)))›
  (is ‹P \ S = ⊥ ⟷ ?rhs›)
proof (subst BOT_iff_Nil_D, intro iffI)
  show ‹[] ∈ D (P \ S) ==> ?rhs›
    by (simp add: D_Hiding)
      (metis (no_types, lifting) filter_empty_conv subsetI)
next
  assume ‹?rhs›
  then obtain t where * : ‹set t ⊆ ev ` S›
    ‹t ∈ D P ∨ (∃f. isInfHiddenRun f P S ∧ t ∈ range f)› by blast
  hence ‹tickFree t ∧ [] = trace_hide t (ev ` S)›
    unfolding tickFree_def by (auto simp add: D_Hiding subset_iff)
  with "*"(2) show ‹[] ∈ D (P \ S)› by (simp add: D_Hiding) metis
qed

lemma event_in_D_Hiding_iff :
  ‹[e] ∈ D (P \ S) ⟷
 P \ S = ⊥ ∨ (∃x t. e = ev x ∧ x ∉ S ∧ [ev x] = trace_hide t (ev ` S) ∧
 (t ∈ D P ∨ (∃f. isInfHiddenRun f P S ∧ t ∈ range f)))›
  (is ‹[e] ∈ D (P \ S) ⟷ P \ S = ⊥ ∨ ?ugly_assertion›)
proof (intro iffI)
  assume assm : ‹[e] ∈ D (P \ S)›
  show ‹P \ S = ⊥ ∨ ?ugly_assertion›
  proof (cases e)
    fix r assume ‹e = 🍋(r)›
    with assm have ‹P \ S = ⊥›
      using BOT_iff_tick_D front_tickFree_Nil is_processT9_tick by blast
    thus ‹P \ S = ⊥ ∨ ?ugly_assertion› by blast
  next
    fix x
    assume ‹e = ev x›
    with assm obtain t u
      where * : ‹front_tickFree u› ‹tickFree t›
        ‹[ev x] = trace_hide t (ev ` S) @ u›
        ‹t ∈ D P ∨ (∃ f. isInfHiddenRun f P S ∧ t ∈ range f)›
      by (simp add: D_Hiding) blast
    from "*"(3) consider ‹set t ⊆ ev ` S› | ‹x ∉ S› ‹ev x ∈ set t›
      by (metis (no_types, lifting) Cons_eq_append_conv empty_filter_conv
          filter_eq_Cons_iff filter_is_subset image_eqI list.set_intros(1) subset_code(1))
    thus ‹P \ S = ⊥ ∨ ?ugly_assertion›
    proof cases
      assume ‹set t ⊆ ev ` S›
      hence ‹P \ S = ⊥› by (meson "*"(4) Hiding_is_BOT_iff)
      thus ‹P \ S = ⊥ ∨ ?ugly_assertion› by blast
    next
      assume ‹x ∉ S› ‹ev x ∈ set t›
      with "*"(3) have ‹[ev x] = trace_hide t (ev ` S)›
        by (induct t) (auto split: if_split_asm)
      with "*"(4) ‹e = ev x› ‹x ∉ S› have ‹?ugly_assertion› by blast
      thus ‹P \ S = ⊥ ∨ ?ugly_assertion› by blast
    qed
  qed
next
  show ‹P \ S = ⊥ ∨ ?ugly_assertion ==> [e] ∈ D (P \ S)›
  proof (elim disjE)
    show ‹P \ S = ⊥ ==> [e] ∈ D (P \ S)› by (simp add: D_BOT)
  next
    show ‹?ugly_assertion ==> [e] ∈ D (P \ S)›
      by (elim exE conjE, simp add: D_Hiding)
        (metis Hiding_tickFree append_Cons append_Nil event_ptick.disc(1)
          front_tickFree_Nil non_tickFree_imp_not_Nil tickFree_Cons_iff)
  qed
qed


text ‹Now we can express term‹initials (P \ S)›.
 This result contains the term term‹P \ S = ⊥› that can be unfolded with
 @{thm [source] Hiding_is_BOT_iff} and the term term‹[ev x] ∈ D (P \ S)›
 that can be unfolded with @{thm [source] event_in_D_Hiding_iff}.›

lemma initials_Hiding:
  ‹(P \ S)⁰ = (if P \ S = ⊥ then UNIV else
 {e. case e of ev x ==> x ∉ S ∧ ([ev x] ∈ D (P \ S) ∨ (∃t. [ev x] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ F P))
 | 🍋(r) ==> ∃t. set t ⊆ ev ` S ∧ t @ [🍋(r)] ∈ T P})›
  (is ‹initials (P \ S) = (if P \ S = ⊥ then UNIV else ?set)›)
proof (split if_split, intro conjI impI)
  show ‹P \ S = ⊥ ==> initials (P \ S) = UNIV› by simp
next
  assume non_BOT : ‹P \ S ≠ ⊥›
  show ‹initials (P \ S) = ?set›
  proof (intro subset_antisym subsetI)
    fix e
    assume initial : ‹e ∈ initials (P \ S)›
      ― ‹This implies prop‹e ∉ ev ` S› with our other assumptions.›
    { fix x
      assume assms : ‹x ∈ S› ‹ev x ∈ initials (P \ S)›
      then consider ‹∃t. [ev x] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ F P›
        | ‹∃t u. front_tickFree u ∧ tickFree t ∧ [ev x] = trace_hide t (ev ` S) @ u ∧
 (t ∈ D P ∨ (∃ f. isInfHiddenRun f P S ∧ t ∈ range f))›
        by (simp add: initials_def T_Hiding) blast
      hence ‹P \ S = ⊥›
      proof cases
        assume ‹∃t. [ev x] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ F P›
        hence False by (metis Cons_eq_filterD image_eqI assms(1))
        thus ‹P \ S = ⊥› by blast
      next
        assume ‹∃t u. front_tickFree u ∧ tickFree t ∧ [ev x] = trace_hide t (ev ` S) @ u ∧
 (t ∈ D P ∨ (∃ f. isInfHiddenRun f P S ∧ t ∈ range f))›
        then obtain t u 
          where * : ‹front_tickFree u› ‹tickFree t› ‹[ev x] = trace_hide t (ev ` S) @ u›
            ‹t ∈ D P ∨ (∃ f. isInfHiddenRun f P S ∧ t ∈ range f)› by blast
        from *(3) have ** : ‹set t ⊆ ev ` S›
          by (induct t) (simp_all add: assms(1) split: if_split_asm)
        from *(4) "**" Hiding_is_BOT_iff show ‹P \ S = ⊥› by blast
      qed
    }
    with initial have * : ‹e ∉ ev ` S› using non_BOT by blast

    from initial consider ‹[e] ∈ D (P \ S)›
      | ‹∃t. [e] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ F P›
      unfolding initials_def by (simp add: T_Hiding D_Hiding) blast
    thus ‹e ∈ ?set›
    proof cases
      assume assm : ‹[e] ∈ D (P \ S)›
      then obtain x where ‹e = ev x›
        by (metis BOT_iff_Nil_D append_Nil event_ptick.exhaust non_BOT process_charn)
      with assm "*" show ‹e ∈ ?set› by (simp add: image_iff)
    next
      assume ‹∃t. [e] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ F P›
      then obtain t where ** : ‹[e] = trace_hide t (ev ` S)›
        ‹(t, ev ` S) ∈ F P› by blast
      thus ‹e ∈ ?set›
      proof (cases e)
        have ‹e = 🍋(r) ==> set (butlast t) ⊆ ev ` S ∧ butlast t @ [🍋(r)] ∈ T P› for r
          using "**" by (cases t rule: rev_cases; simp add: F_T empty_filter_conv subset_eq split: if_split_asm)
            (metis F_T Hiding_tickFree append_T_imp_tickFree neq_Nil_conv non_tickFree_tick)
        thus ‹e = 🍋(r) ==> e ∈ ?set› for r by auto
      next
        fix x
        assume ‹e = ev x›
        with "*" have ‹x ∉ S› by blast
        with ‹e = ev x› "**"(1) "**"(2) show ‹e ∈ ?set› by auto
      qed
    qed
  next
    fix e
    assume ‹e ∈ ?set›
    then consider r where ‹e = 🍋(r)› ‹∃t. set t ⊆ ev ` S ∧ t @ [🍋(r)] ∈ T P›
      | a where ‹e = ev a› ‹a ∉ S›
        ‹[ev a] ∈ D (P \ S) ∨
 (∃t. [ev a] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ F P)› by (cases e) simp_all
    thus ‹e ∈ initials (P \ S)›
    proof cases
      fix r assume assms : ‹e = 🍋(r)› ‹∃t. set t ⊆ ev ` S ∧ t @ [🍋(r)] ∈ T P›
      from assms(2) obtain t
        where * : ‹set t ⊆ ev ` S› ‹t @ [🍋(r)] ∈ T P› by blast
      have ** : ‹[e] = trace_hide (t @ [🍋(r)]) (ev ` S) ∧ (t @ [🍋(r)], ev ` S) ∈ F P›
        using "*"(1) by (simp add: assms(1) image_iff tick_T_F[OF "*"(2)] subset_iff)
      show ‹e ∈ initials (P \ S)›
        unfolding initials_def by (simp add: T_Hiding) (use "**" in blast)
    next
      show ‹[ev a] ∈ D (P \ S) ∨
 (∃t. [ev a] = trace_hide t (ev ` S) ∧ (t, ev ` S) ∈ F P) ==> e ∈ (P \ S)⁰›
        if ‹e = ev a› for a
      proof (elim exE conjE disjE)
        show ‹[ev a] ∈ D (P \ S) ==> e ∈ (P \ S)⁰›
          by (simp add: ‹e = ev a› D_T initials_memI')
      next
        show ‹[ev a] = trace_hide t (ev ` S) ==> (t, ev ` S) ∈ F P ==> e ∈ (P \ S)⁰› for t
          by (metis F_T initials_memI' mem_T_imp_mem_T_Hiding ‹e = ev a›)
      qed
    qed
  qed
qed


text ‹In the end the result would look something like this:

 @{thm initials_Hiding[unfolded event_in_D_Hiding_iff Hiding_is_BOT_iff, no_vars]}›

text ‹Obviously, it is not very easy to use. We will therefore rely more on the corollaries below.›

corollary initial_tick_Hiding_iff :
  ‹🍋(r) ∈ (P \ B)⁰ ⟷ P \ B = ⊥ ∨ (∃t. set t ⊆ ev ` B ∧ t @ [🍋(r)] ∈ T P)›
  by (simp add: initials_Hiding)

corollary initial_tick_imp_initial_tick_Hiding:
  ‹🍋(r) ∈ P⁰ ==> 🍋(r) ∈ (P \ B)⁰›
  by (subst initials_Hiding, simp add: initials_def)
    (metis append_Nil empty_iff empty_set subset_iff)


corollary initial_inside_Hiding_iff :
  ‹e ∈ S ==> ev e ∈ (P \ S)⁰ ⟷ P \ S = ⊥›
  by (simp add: initials_Hiding)


corollary initial_notin_Hiding_iff :
  ‹e ∉ S ==> ev e ∈ (P \ S)⁰ ⟷
 P \ S = ⊥ ∨
 (∃t. [ev e] = trace_hide t (ev ` S) ∧
 (t ∈ D P ∨ (∃f. isInfHiddenRun f P S ∧ t ∈ range f) ∨ (t, ev ` S) ∈ F P))›
  by (auto simp add: initials_Hiding event_in_D_Hiding_iff split: if_split_asm)


corollary initial_notin_imp_initial_Hiding:
  ‹ev e ∈ (P \ S)⁰› if initial : ‹ev e ∈ P⁰› and notin : ‹e ∉ S›
proof -
  from inf_hidden[of S ‹[ev e]› P]
  consider f where ‹isInfHiddenRun f P S› ‹[ev e] ∈ range f›  
    | t where ‹[ev e] = trace_hide t (ev ` S)› ‹(t, ev ` S) ∈ F P›
    by (simp add: initials_Hiding image_iff[of ‹ev e›] notin)
      (metis mem_Collect_eq initial initials_def)
  thus ‹ev e ∈ initials (P \ S)›
  proof cases
    show ‹ev e ∈ (P \ S)⁰› if ‹isInfHiddenRun f P S› ‹[ev e] ∈ range f› for f
    proof (intro initials_memI[of ‹ev e› ‹[]›] D_T)
      from that show ‹[ev e] ∈ D (P \ S)›
        by (simp add: event_in_D_Hiding_iff image_iff[of ‹ev e›] notin)
          (metis (no_types, lifting) event_ptick.inject(1) filter.simps image_iff notin)
    qed
  next
    show ‹[ev e] = trace_hide t (ev ` S) ==> (t, ev ` S) ∈ F P ==> ev e ∈ (P \ S)⁰› for t
      by (auto simp add: initials_Hiding notin)
  qed
qed  



section ‹Behaviour of const‹initials› with Operators of session‹HOL-CSPM››

lemma initials_GlobalDet:
  ‹(◻a ∈ A. P a)⁰ = (∪a ∈ A. initials (P a))›
  by (auto simp add: initials_def T_GlobalDet)

lemma initials_GlobalNdet:
  ‹(⊓a ∈ A. P a)⁰ = (∪a ∈ A. initials (P a))›
  by (auto simp add: initials_def T_GlobalNdet)



(* lemma initials_MultiSeq:
  \<open>initials (SEQ l \<in>@ L. P l) =
   (let i = first_elem (\<lambda>l. \<checkmark> \<notin> initials (P l)) L
     in   if (\<exists>j < i. P (L ! j) = \<bottom>)
        then UNIV 
        else let S = (\<Union>l \<in> set (take (Suc i) L). initials (P l)) - {\<checkmark>}
              in if i < length L then S else insert \<checkmark> S)\<close>
  unfolding Let_def
proof (induct L)
  case Nil
  thus ?case by (simp add: initials_SKIP SKIP_neq_BOT)
next
  case (Cons l L)
  show ?case
    apply (simp add: initials_Seq initials_BOT local.Cons, intro conjI impI)
           apply ((metis nth_Cons_0 zero_less_Suc)+)[1]
          apply ((metis Suc_less_eq nth_Cons_Suc)+)[2]
        apply (metis nth_Cons_0 zero_less_Suc)
    by (metis less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc, blast)+
qed *)


lemma initials_MultiSync:
  ‹initials (\[S\] m ∈# M. P m) =
 ( if M = {#} then {}
 else if ∃m ∈# M. P m = ⊥ then UNIV
 else if ∃m. M = {#m#} then initials (P (THE m. M = {#m#}))
 else {e. ∃m ∈# M. e ∈ initials (P m) - (range tick ∪ ev ` S)} ∪
 {e ∈ range tick ∪ ev ` S. ∀m ∈# M. e ∈ initials (P m)})›
proof -
  have * : ‹initials (\[S\] m ∈# (M + {#a, a'#}). P m) =
 {e. ∃m ∈# M + {#a, a'#}. e ∈ initials (P m) - (range tick ∪ ev ` S)} ∪
 {e ∈ range tick ∪ ev ` S. ∀m ∈# M + {#a, a'#}. e ∈ initials (P m)}›
    if non_BOT : ‹∀m ∈# M + {#a, a'#}. P m ≠ ⊥› for a a' M
  proof (induct M rule: msubset_induct'[OF subset_mset.refl])
    case 1
    then show ?case by (auto simp add: non_BOT initials_Sync)
  next
    case (2 a'' M')
    have * : ‹MultiSync S (add_mset a'' M' + {#a, a'#}) P =
 P a'' [S] (MultiSync S (M' + {#a, a'#}) P)›
      by (simp add: add_mset_commute)
    have ** : ‹¬ (P a'' = ⊥ ∨ MultiSync S (M' + {#a, a'#}) P = ⊥)›
      using "2.hyps"(1, 2) in_diffD non_BOT 
      by (auto simp add: MultiSync_is_BOT_iff Sync_is_BOT_iff, fastforce, meson mset_subset_eqD)
    show ?case
      by (auto simp only: * initials_Sync ** "2.hyps"(3), auto)
  qed

  show ?thesis
  proof (cases ‹∃m ∈# M. P m = ⊥›)
    show ‹∃m ∈# M. P m = ⊥ ==> ?thesis›
      by simp (metis MultiSync_BOT_absorb initials_BOT)
  next
    show ‹¬ (∃m∈#M. P m = ⊥) ==> ?thesis›
    proof (cases ‹∃a a' M'. M = M' + {#a, a'#}›)
      assume assms : ‹¬ (∃m∈#M. P m = ⊥)› ‹∃a a' M'. M = M' + {#a, a'#}›
      from assms(2) obtain a a' M' where ‹M = M' + {#a, a'#}› by blast
      with * assms(1) show ?thesis by simp
    next
      assume ‹∄a a' M'. M = M' + {#a, a'#}›
      hence ‹M = {#} ∨ (∃m. M = {#m#})›
        by (metis add.right_neutral multiset_cases union_mset_add_mset_right)
      thus ?thesis by auto
    qed
  qed
qed



lemma initials_Throw : ‹(P Θ a ∈ A. Q a)⁰ = P⁰›
proof (cases ‹P = ⊥›)
  show ‹P = ⊥ ==> (P Θ a ∈ A. Q a)⁰ = P⁰› by simp
next
  show ‹(P Θ a ∈ A. Q a)⁰ = P⁰› if ‹P ≠ ⊥›
  proof (intro subset_antisym subsetI)
    from ‹P ≠ ⊥› show ‹e ∈ (P Θ a ∈ A. Q a)⁰ ==> e ∈ P⁰› for e
      by (auto simp add: T_Throw D_T is_processT7 Cons_eq_append_conv BOT_iff_Nil_D
          intro!: initials_memI' dest!: initials_memD)
  next
    show ‹e ∈ P⁰ ==> e ∈ (P Θ a ∈ A. Q a)⁰› for e
      by (auto simp add: initials_memD T_Throw Cons_eq_append_conv
          intro!: initials_memI')
  qed
qed


lemma initials_Interrupt: ‹(P △ Q)⁰ = P⁰ ∪ Q⁰›
proof (intro subset_antisym subsetI)
  show ‹e ∈ (P △ Q)⁰ ==> e ∈ P⁰ ∪ Q⁰› for e
    by (auto simp add: T_Interrupt Cons_eq_append_conv
        dest!: initials_memD intro: initials_memI)
next
  show ‹e ∈ P⁰ ∪ Q⁰ ==> e ∈ (P △ Q)⁰› for e
    by (force simp add: initials_def T_Interrupt)
qed







section ‹Behaviour of const‹initials› with Reference Processes›

lemma initials_DF: ‹(DF A)⁰ = ev ` A›
  by (subst DF_unfold) (simp add: initials_Mndetprefix)

lemma initials_DF_SKIPS: ‹(DF_SKIPS A R)⁰ = ev ` A ∪ tick ` R›
  by (subst DF_{SKIPS_unfold})
    (simp add: initials_Mndetprefix initials_Ndet)

lemma initials_RUN: ‹(RUN A)⁰ = ev ` A›
  by (subst RUN_unfold) (simp add: initials_Mprefix)

lemma initials_CHAOS: ‹(CHAOS A)⁰ = ev ` A›
  by (subst CHAOS_unfold)
    (simp add: initials_Mprefix initials_Ndet)

lemma initials_CHAOS_SKIPS: ‹(CHAOS_SKIPS A R)⁰ = ev ` A ∪ tick ` R›
  by (subst CHAOS_{SKIPS_unfold})
    (auto simp add: initials_Mprefix initials_Ndet)


lemma empty_ev_initials_iff_empty_events_of :
  ‹{a. ev a ∈ P⁰} = {} ⟷ α(P) = {}›
proof (rule iffI)
  show ‹α(P) = {} ==> {a. ev a ∈ P⁰} = {}›
    by (auto simp add: initials_def events_of_def)
next
  show ‹α(P) = {}› if ‹{a. ev a ∈ P⁰} = {}›
  proof (rule ccontr)
    assume ‹α(P) ≠ {}›
    then obtain a t where ‹t ∈ T P› ‹ev a ∈ set t›
      by (meson equals0I events_of_memD)
    from ‹t ∈ T P› consider ‹t = []› | r where ‹t = [🍋(r)]› | b t' where ‹t = ev b # t'›
      by (metis T_imp_front_tickFree ‹ev a ∈ set t› front_tickFree_Cons_iff
          is_ev_def list.distinct(1) list.set_cases)
    thus False
    proof cases
      from ‹ev a ∈ set t› show ‹t = [] ==> False› by simp
    next
      from ‹ev a ∈ set t› show ‹t = [🍋(r)] ==> False› for r by simp
    next
      fix b t' assume ‹t = ev b # t'›
      with ‹t ∈ T P› have ‹b ∈ {a. ev a ∈ P⁰}› by (simp add: initials_memI)
      with ‹{a. ev a ∈ P⁰} = {}› show False by simp
    qed
  qed
qed



section ‹Properties of const‹initials› related to continuity›

text ‹We prove here some properties that we will need later in continuity or admissibility proofs.›

lemma initials_LUB:
  ‹chain Y ==> (⊔i. Y i)⁰ = (∩P ∈ (range Y). P⁰)›
  unfolding initials_def by (auto simp add: limproc_is_thelub T_LUB)


lemma adm_in_F: ‹cont u ==> adm (λx. (s, X) ∈ F (u x))›
  by (simp add: adm_def cont2contlubE limproc_is_thelub ch2ch_cont F_LUB)

lemma adm_in_D: ‹cont u ==> adm (λx. s ∈ D (u x))›
  by (simp add: D_LUB_2 adm_def ch2ch_cont cont2contlubE limproc_is_thelub)

lemma adm_in_T: ‹cont u ==> adm (λx. s ∈ T (u x))›
  by (fold T_F_spec) (fact adm_in_F)

lemma initial_adm[simp] : ‹cont u ==> adm (λx. e ∈ (u x)⁰)›
  unfolding initials_def by (simp add: adm_in_T)


(*<*)
end
  (*>*)