Theory RS_Trace_Model_CSP

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 * Author: Benjamin Puyobro, Université Paris-Saclay,
           IRT SystemX, CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 *
 * 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
 *
 * * 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.
 *
 * 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 HOLDER 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.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


section ‹Trace Model of CSP›

(*<*)
theory RS_Trace_Model_CSP
  imports Restriction_Spaces "HOL-Library.Prefix_Order"
begin 
  (*>*)

text ‹
In the AFP one can already find ▩‹HOL-CSP›, a shallow embedding of the failure-divergence
model of denotational semantics proposed by Hoare, Roscoe and Brookes in the eighties.
Here, we simplify the example by restraining ourselves to a trace model.›

subsection ‹Prerequisites›

datatype 'a event = ev (of_ev : 'a) | tick (‹✓›)

type_synonym 'a trace = ‹'a event list›


definition tickFree :: ‹'a trace ⇒ bool› (‹tF›)
  where ‹tickFree t ≡ ✓ ∉ set t›

definition front_tickFree :: ‹'a trace ⇒ bool› (‹ftF›)
  where ‹front_tickFree s ≡ s = [] ∨ tickFree (tl (rev s))›


lemma tickFree_Nil        [simp] : ‹tF []›
  and tickFree_Cons_iff   [simp] : ‹tF (a # t) ⟷ a ≠ ✓ ∧ tF t›
  and tickFree_append_iff [simp] : ‹tF (s @ t) ⟷ tF s    ∧ tF t›
  and tickFree_rev_iff    [simp] : ‹tF (rev t) ⟷ tF t›
  and non_tickFree_tick   [simp] : ‹¬ tF [✓]›
  by (auto simp add: tickFree_def)

lemma tickFree_iff_is_map_ev : ‹tF t ⟷ (∃u. t = map ev u)›
  by (metis event.collapse event.distinct(1) ex_map_conv tickFree_def)

lemma front_tickFree_Nil   [simp] : ‹ftF []›
  and front_tickFree_single[simp] : ‹ftF [a]›
  by (simp_all add: front_tickFree_def)


lemma tickFree_tl : ‹tF s ⟹ tF (tl s)›
  by (cases s) simp_all

lemma non_tickFree_imp_not_Nil: ‹¬ tF s ⟹ s ≠ []›
  using tickFree_Nil by blast

lemma tickFree_butlast: ‹tF s ⟷ tF (butlast s) ∧ (s ≠ [] ⟶ last s ≠ ✓)›
  by (induct s) simp_all

lemma front_tickFree_iff_tickFree_butlast: ‹ftF s ⟷ tF (butlast s)›
  by (induct s) (auto simp add: front_tickFree_def)

lemma front_tickFree_Cons_iff: ‹ftF (a # s) ⟷ s = [] ∨ a ≠ ✓ ∧ ftF s›
  by (simp add: front_tickFree_iff_tickFree_butlast)

lemma front_tickFree_append_iff:
  ‹ftF (s @ t) ⟷ (if t = [] then ftF s else tF s ∧ ftF t)›
  by (simp add: butlast_append front_tickFree_iff_tickFree_butlast)

lemma tickFree_imp_front_tickFree [simp] : ‹tF s ⟹ ftF s›
  by (simp add: front_tickFree_def tickFree_tl)

lemma front_tickFree_charn: ‹ftF s ⟷ s = [] ∨ (∃a t. s = t @ [a] ∧ tF t)›
  by (cases s rule: rev_cases) (simp_all add: front_tickFree_def)


lemma nonTickFree_n_frontTickFree: ‹¬ tF s ⟹ ftF s ⟹ ∃t r. s = t @ [✓]›
  by (metis front_tickFree_charn tickFree_Cons_iff
      tickFree_Nil tickFree_append_iff)

lemma front_tickFree_dw_closed : ‹ftF (s @ t) ⟹ ftF s›
  by (metis front_tickFree_append_iff tickFree_imp_front_tickFree)

lemma front_tickFree_append: ‹tF s ⟹ ftF t ⟹ ftF (s @ t)›
  by (simp add: front_tickFree_append_iff)

lemma tickFree_imp_front_tickFree_snoc: ‹tF s ⟹ ftF (s @ [a])›
  by (simp add: front_tickFree_append)

lemma front_tickFree_nonempty_append_imp: ‹ftF (t @ r) ⟹ r ≠ [] ⟹ tF t ∧ ftF r›
  by (simp add: front_tickFree_append_iff)

lemma tickFree_map_ev [simp] : ‹tF (map ev t)›
  by (induct t) simp_all

lemma tickFree_map_ev_comp [simp] : ‹tF (map (ev ∘ f) t)›
  by (metis list.map_comp tickFree_map_ev)

lemma front_tickFree_map_map_event_iff :
  ‹ftF (map (map_event f) t) ⟷ ftF t›
  by (induct t) (simp_all add: front_tickFree_Cons_iff)




definition is_process :: ‹'a trace set ⇒ bool›
  where ‹is_process T ≡ [] ∈ T ∧ (∀t. t ∈ T ⟶ ftF t) ∧ (∀t u. t @ u ∈ T ⟶ t ∈ T)›

typedef 'a process = ‹{T :: 'a trace set. is_process T}›
  morphisms Traces to_process
proof (rule exI)
  show ‹{[]} ∈ {T. is_process T}›
    by (simp add: is_process_def front_tickFree_def)
qed

setup_lifting type_definition_process


notation Traces (‹𝒯›)

lemma is_process_inv :
  ‹[] ∈ 𝒯 P ∧ (∀t. t ∈ 𝒯 P ⟶ ftF t) ∧ (∀t u. t @ u ∈ 𝒯 P ⟶ t ∈ 𝒯 P)›
  by (metis is_process_def mem_Collect_eq to_process_cases to_process_inverse)

lemma Nil_elem_T       : ‹[] ∈ 𝒯 P›
  and front_tickFree_T : ‹t ∈ 𝒯 P ⟹ ftF t›
  and T_dw_closed      : ‹t @ u ∈ 𝒯 P ⟹ t ∈ 𝒯 P›
  by (simp_all add: is_process_inv)


lemma process_eq_spec : ‹P = Q ⟷ 𝒯 P = 𝒯 Q›
  by transfer simp



subsection ‹First Processes›

lift_definition BOT :: ‹'a process› is ‹{t. ftF t}›
  by (auto simp add: is_process_def front_tickFree_append_iff)

lemma T_BOT : ‹𝒯 BOT = {t. ftF t}›
  by (simp add: BOT.rep_eq)


lift_definition SKIP :: ‹'a process› is ‹{[], [✓]}›
  by (simp add: is_process_def append_eq_Cons_conv)

lemma T_SKIP : ‹𝒯 SKIP = {[], [✓]}›
  by (simp add: SKIP.rep_eq)


lift_definition STOP :: ‹'a process› is ‹{[]}›
  by (simp add: is_process_def)

lemma T_STOP : ‹𝒯 STOP = {[]}›
  by (simp add: STOP.rep_eq)


lift_definition Sup_processes ::
  ‹(nat ⇒ 'a process) ⇒ 'a process› is ‹λσ. ⋂i. 𝒯 (σ i)›
proof -
  show ‹is_process (⋂i. 𝒯 (σ i))› for σ :: ‹nat ⇒ 'a process›
  proof (unfold is_process_def, intro conjI allI impI)
    show ‹[] ∈ (⋂i. 𝒯 (σ i))› by (simp add: Nil_elem_T)
  next
    show ‹t ∈ (⋂i. 𝒯 (σ i)) ⟹ ftF t› for t
      by (auto intro: front_tickFree_T)
  next
    show ‹t @ u ∈ (⋂i. 𝒯 (σ i)) ⟹ t ∈ (⋂i. 𝒯 (σ i))› for t u
      by (auto intro: T_dw_closed)
  qed
qed

lemma T_Sup_processes : ‹𝒯 (Sup_processes σ) = (⋂i. 𝒯 (σ i))›
  by (simp add: Sup_processes.rep_eq)



subsection ‹Instantiations›

instantiation process :: (type) order
begin

definition less_eq_process :: ‹'a process ⇒ 'a process ⇒ bool›
  where ‹P ≤ Q ≡ 𝒯 Q ⊆ 𝒯 P›

definition less_process :: ‹'a process ⇒ 'a process ⇒ bool›
  where ‹P < Q ≡ 𝒯 Q ⊂ 𝒯 P›

instance
  by intro_classes
    (auto simp add: less_eq_process_def less_process_def process_eq_spec)

end


instantiation process :: (type) order_restriction_space
begin

lift_definition restriction_process :: ‹'a process ⇒ nat ⇒ 'a process›
  is ‹λP n. 𝒯 P ∪ {t @ u |t u. t ∈ 𝒯 P ∧ length t = n ∧ tF t ∧ ftF u}›
proof -
  show ‹?thesis P n› (is ‹is_process ?t›) for P n
  proof (unfold is_process_def, intro conjI allI impI)
    show ‹[] ∈ ?t› by (simp add: Nil_elem_T)
  next
    show ‹t ∈ ?t ⟹ ftF t› for t
      by (auto simp add: front_tickFree_append_iff front_tickFree_T)
  next
    fix t u assume ‹t @ u ∈ ?t›
    then consider ‹t @ u ∈ 𝒯 P›
      | (@) t' u' where ‹t @ u = t' @ u'› ‹t' ∈ 𝒯 P›
        ‹length t' = n› ‹tF t'› ‹ftF u'› by blast
    thus ‹t ∈ ?t›
    proof cases
      from T_dw_closed show ‹t @ u ∈ 𝒯 P ⟹ t ∈ ?t› by blast
    next
      case @
      show ‹t ∈ ?t›
      proof (cases ‹length t ≤ length t'›)
        assume ‹length t ≤ length t'›
        with "@"(1) obtain t'' where ‹t' = t @ t''›
          by (metis append_eq_append_conv_if append_eq_conv_conj)
        with "@"(2) T_dw_closed show ‹t ∈ ?t› by blast
      next
        assume ‹¬ length t ≤ length t'›
        hence ‹length t' ≤ length t› by simp
        with "@"(1,4,5) ‹¬ length t ≤ length t'›
        obtain t'' where ‹t = t' @ t''› ‹ftF t''›
          by (metis append_eq_conv_conj drop_eq_Nil front_tickFree_append
              front_tickFree_dw_closed front_tickFree_nonempty_append_imp
              take_all_iff take_append)
        with "@"(2,3,4) show ‹t ∈ ?t› by blast
      qed
    qed
  qed
qed

lemma T_restriction_process :
  ‹𝒯 (P ↓ n) = 𝒯 P ∪ {t @ u |t u. t ∈ 𝒯 P ∧ length t = n ∧ tF t ∧ ftF u}›
  by (simp add: restriction_process.rep_eq)


lemma restriction_process_0 [simp] : ‹P ↓ 0 = BOT›
  by transfer (auto simp add: front_tickFree_T Nil_elem_T)

lemma T_restriction_processE :
  ‹t ∈ 𝒯 (P ↓ n) ⟹
   (t ∈ 𝒯 P ⟹ length t ≤ n ⟹ thesis) ⟹
   (⋀u v. t = u @ v ⟹ u ∈ 𝒯 P ⟹ length u = n ⟹ tF u ⟹ ftF v ⟹ thesis) ⟹
   thesis›
  by (simp add: T_restriction_process)
    (metis (no_types) T_dw_closed append_take_drop_id drop_eq_Nil
      front_tickFree_T front_tickFree_nonempty_append_imp length_take min_def)


instance
proof intro_classes
  show ‹P ↓ 0 ≤ Q ↓ 0› for P Q :: ‹'a process› by simp
next
  show ‹P ↓ n ↓ m = P ↓ min n m› for P :: ‹'a process› and n m
  proof (subst process_eq_spec, intro subset_antisym subsetI)
    show ‹t ∈ 𝒯 (P ↓ n ↓ m) ⟹ t ∈ 𝒯 (P ↓ min n m)› for t
      by (elim T_restriction_processE)
        (auto simp add: T_restriction_process intro: front_tickFree_append)
  next
    show ‹t ∈ 𝒯 (P ↓ min n m) ⟹ t ∈ 𝒯 (P ↓ n ↓ m)› for t
      by (elim T_restriction_processE)
        (auto simp add: T_restriction_process min_def split: if_split_asm)
  qed
next
  show ‹P ≤ Q ⟹ P ↓ n ≤ Q ↓ n› for P Q :: ‹'a process› and n
    by (auto simp add: less_eq_process_def T_restriction_process)
next
  fix P Q :: ‹'a process› assume ‹¬ P ≤ Q›
  then obtain t where ‹t ∈ 𝒯 Q› ‹t ∉ 𝒯 P›
    unfolding less_eq_process_def by blast
  hence ‹t ∈ 𝒯 (Q ↓ Suc (length t)) ∧ t ∉ 𝒯 (P ↓ Suc (length t))›
    by (auto simp add: T_restriction_process) 
  hence ‹¬ P ↓ Suc (length t) ≤ Q ↓ Suc (length t)›
    unfolding less_eq_process_def by blast
  thus ‹∃n. ¬ P ↓ n ≤ Q ↓ n› ..
qed


text ‹Of course, we recover the structure of \<^class>‹restriction_space›.›

lemma ‹OFCLASS ('a process, restriction_space_class)›
  by intro_classes

end


lemma restricted_Sup_processes_is :
  ‹(λn. Sup_processes σ ↓ n) = σ› if ‹restriction_chain σ›
proof (subst (2) restricted_restriction_chain_is
    [OF ‹restriction_chain σ›, symmetric], rule ext)
  fix n
  have ‹length t ≤ n ⟹ t ∈ 𝒯 (σ n) ⟷ (∀i. t ∈ 𝒯 (σ i))› for t n
  proof safe
    show ‹t ∈ 𝒯 (σ i)› if ‹length t ≤ n› ‹t ∈ 𝒯 (σ n)› for i
    proof (cases ‹i ≤ n›)
      from restriction_chain_def_ter[THEN iffD1, OF ‹restriction_chain σ›]
      show ‹i ≤ n ⟹ t ∈ 𝒯 (σ i)›
        by (metis (lifting) ‹t ∈ 𝒯 (σ n)› T_restriction_process Un_iff)
    next
      from ‹length t ≤ n› ‹t ∈ 𝒯 (σ n)› show ‹¬ i ≤ n ⟹ t ∈ 𝒯 (σ i)›
        by (induct n, simp_all add: Nil_elem_T)
          (metis (no_types) T_restriction_processE
            append_eq_conv_conj linorder_linear take_all_iff
            restriction_chain_def_ter[THEN iffD1, OF ‹restriction_chain σ›])
    qed
  next
    show ‹∀i. t ∈ 𝒯 (σ i) ⟹ t ∈ 𝒯 (σ n)› by simp
  qed
  hence * : ‹length t ≤ n ⟹ t ∈ 𝒯 (σ n) ⟷ t ∈ 𝒯 (Sup_processes σ)› for t n
    by (simp add: T_Sup_processes)

  show ‹Sup_processes σ ↓ n = σ n ↓ n› for n
  proof (subst process_eq_spec, intro subset_antisym subsetI)
    show ‹t ∈ 𝒯 (Sup_processes σ ↓ n) ⟹ t ∈ 𝒯 (σ n ↓ n)› for t
    proof (elim T_restriction_processE)
      show ‹t ∈ 𝒯 (Sup_processes σ) ⟹ length t ≤ n ⟹ t ∈ 𝒯 (σ n ↓ n)›
        by (simp add: "*" T_restriction_process)
    next
      show ‹⟦t = u @ v; u ∈ 𝒯 (Sup_processes σ); length u = n; tF u; ftF v⟧
            ⟹ t ∈ 𝒯 (σ n ↓ n)› for u v
        by (auto simp add: "*" T_restriction_process)
    qed
  next
    from "*" show ‹t ∈ 𝒯 (σ n ↓ n) ⟹ t ∈ 𝒯 (Sup_processes σ ↓ n)› for t
      by (elim T_restriction_processE)
        (auto simp add: T_restriction_process)
  qed
qed


instance process :: (type) complete_restriction_space 
proof intro_classes
  show ‹restriction_convergent σ› if ‹restriction_chain σ›
    for σ :: ‹nat ⇒ 'a process›
  proof (rule restriction_convergentI)
    have ‹σ = (λn. Sup_processes σ ↓ n)›
      by (simp add: restricted_Sup_processes_is ‹restriction_chain σ›)
    moreover have ‹(λn. Sup_processes σ ↓ n) ─↓→ Sup_processes σ›
      by (fact restriction_tendsto_restrictions)
    ultimately show ‹σ ─↓→ Sup_processes σ› by simp
  qed
qed



subsection ‹Operators›

lift_definition Choice :: ‹'a process ⇒ 'a process ⇒ 'a process› (infixl ‹□› 82)
  is ‹λP Q. 𝒯 P ∪ 𝒯 Q›
  by (auto simp add: is_process_def Nil_elem_T front_tickFree_T intro: T_dw_closed)

lemma T_Choice : ‹𝒯 (P □ Q) = 𝒯 P ∪ 𝒯 Q›
  by (simp add: Choice.rep_eq)


lift_definition GlobalChoice :: ‹['b set, 'b ⇒ 'a process] ⇒ 'a process›
  is ‹λA P. if A = {} then {[]} else ⋃a∈A. 𝒯 (P a)›
  by (auto simp add: is_process_def Nil_elem_T front_tickFree_T intro: T_dw_closed)

syntax "_GlobalChoice" :: ‹[pttrn, 'b set, 'a process] ⇒ 'a process›
  (‹(3□((_)/∈(_))./ (_))› [78,78,77] 77)
syntax_consts "_GlobalChoice" ⇌ GlobalChoice
translations  "□ a ∈ A. P" ⇌ "CONST GlobalChoice A (λa. P)"

lemma T_GlobalChoice : ‹𝒯 (□a ∈ A. P a) = (if A = {} then {[]} else ⋃a∈A. 𝒯 (P a))›
  by (simp add: GlobalChoice.rep_eq)


lift_definition Seq :: ‹'a process ⇒ 'a process ⇒ 'a process› (infixl ‹❙;› 74)
  is ‹λP Q. {t ∈ 𝒯 P. tF t} ∪ {t @ u |t u. t @ [✓] ∈ 𝒯 P ∧ u ∈ 𝒯 Q}›
  by (auto simp add: is_process_def Nil_elem_T append_eq_append_conv2 intro: T_dw_closed)
    (metis front_tickFree_T front_tickFree_append_iff
      front_tickFree_dw_closed not_Cons_self,
      meson front_tickFree_append_iff is_process_inv snoc_eq_iff_butlast)

lemma T_Seq : ‹𝒯 (P ❙; Q) = {t ∈ 𝒯 P. tF t} ∪ {t @ u |t u. t @ [✓] ∈ 𝒯 P ∧ u ∈ 𝒯 Q}›
  by (simp add: Seq.rep_eq)


lift_definition Renaming :: ‹['a process, 'a ⇒ 'b] ⇒ 'b process›
  is ‹λP f. {map (map_event f) u |u. u ∈ 𝒯 P}›
  by (auto simp add: is_process_def Nil_elem_T front_tickFree_map_map_event_iff
      front_tickFree_T append_eq_map_conv intro: T_dw_closed)

lemma T_Renaming : ‹𝒯 (Renaming P f) = {map (map_event f) u |u. u ∈ 𝒯 P}›
  by (simp add: Renaming.rep_eq)


lift_definition Mprefix :: ‹['a set, 'a ⇒ 'a process] ⇒ 'a process›
  is ‹λA P. insert [] {ev a # t |a t. a ∈ A ∧ t ∈ 𝒯 (P a)}›
  by (auto simp add: is_process_def front_tickFree_Cons_iff
      front_tickFree_T append_eq_Cons_conv intro: T_dw_closed)

syntax "_Mprefix" :: ‹[pttrn, 'a set, 'a process] ⇒ 'a process›	
  (‹(3□((_)/∈(_))/ → (_))› [78,78,77] 77)
syntax_consts "_Mprefix" ⇌ Mprefix
translations "□a∈A → P" ⇌ "CONST Mprefix A (λa. P)"

lemma T_Mprefix : ‹𝒯 (□a ∈ A → P a) = insert [] {ev a # t |a t. a ∈ A ∧ t ∈ 𝒯 (P a)}›
  by (simp add: Mprefix.rep_eq)






fun setinterleaving :: ‹'a trace × 'a set × 'a trace ⇒ 'a trace set›
  where Nil_setinterleaving_Nil : ‹setinterleaving ([], A, []) = {[]}›

|     ev_setinterleaving_Nil :
  ‹setinterleaving (ev a # u, A, []) =
         (if a ∈ A then {} else {ev a # t| t. t ∈ setinterleaving (u, A, [])})›
|     tick_setinterleaving_Nil : ‹setinterleaving (✓ # u, A, []) = {}›

|     Nil_setinterleaving_ev :
  ‹setinterleaving ([], A, ev b # v) =
         (if b ∈ A then {} else {ev b # t| t. t ∈ setinterleaving ([], A, v)})›
|     Nil_setinterleaving_tick  : ‹setinterleaving ([], A, ✓ # v) = {}›

|     ev_setinterleaving_ev : 
  ‹setinterleaving (ev a # u, A, ev b # v) =
         (  if a ∈ A
          then   if b ∈ A 
                then   if a = b
                     then {ev a # t |t. t ∈ setinterleaving (u, A, v)}
                     else {}
                else {ev b # t |t. t ∈ setinterleaving (ev a # u, A, v)}
           else   if b ∈ A then {ev a # t |t. t ∈ setinterleaving (u, A, ev b # v)}
                else {ev a # t |t. t ∈ setinterleaving (u, A, ev b # v)} ∪
                     {ev b # t |t. t ∈ setinterleaving (ev a # u, A, v)})›
|     ev_setinterleaving_tick :
  ‹setinterleaving (ev a # u, A, ✓ # v) =
         (if a ∈ A then {} else {ev a # t |t. t ∈ setinterleaving (u, A, ✓ # v)})›
|     tick_setinterleaving_ev :
  ‹setinterleaving (✓ # u, A, ev b # v) =
         (if b ∈ A then {} else {ev b # t |t. t ∈ setinterleaving (✓ # u, A, v)})›
|     tick_setinterleaving_tick :
  ‹setinterleaving (✓ # u, A, ✓ # v) = {✓ # t |t. t ∈ setinterleaving (u, A, v)}›


lemmas setinterleaving_induct
  [case_names Nil_setinterleaving_Nil ev_setinterleaving_Nil tick_setinterleaving_Nil
    Nil_setinterleaving_ev Nil_setinterleaving_tick ev_setinterleaving_ev
    ev_setinterleaving_tick tick_setinterleaving_ev tick_setinterleaving_tick] =
  setinterleaving.induct



lemma Cons_setinterleaving_Nil :
  ‹setinterleaving (e # u, A, []) =
   (case e of ev a ⇒ (  if a ∈ A then {}
                       else {ev a # t |t. t ∈ setinterleaving (u, A, [])})
            | ✓ ⇒ {})›
  by (cases e) simp_all

lemma Nil_setinterleaving_Cons :
  ‹setinterleaving ([], A, e # v) =
   (case e of ev a ⇒ (  if a ∈ A then {}
                       else {ev a # t |t. t ∈ setinterleaving ([], A, v)})
            | ✓ ⇒ {})›
  by (cases e) simp_all

lemma Cons_setinterleaving_Cons :
  ‹setinterleaving (e # u, A, f # v) =
   (case e of ev a ⇒
    (case f of ev b ⇒ 
       if a ∈ A
     then   if b ∈ A 
           then   if a = b
                then {ev a # t |t. t ∈ setinterleaving (u, A, v)}
                else {}
           else {ev b # t |t. t ∈ setinterleaving (ev a # u, A, v)}
      else   if b ∈ A then {ev a # t |t. t ∈ setinterleaving (u, A, ev b # v)}
           else {ev a # t |t. t ∈ setinterleaving (u, A, ev b # v)} ∪
                {ev b # t |t. t ∈ setinterleaving (ev a # u, A, v)}
             | ✓ ⇒   if a ∈ A then {}
                    else {ev a # t |t. t ∈ setinterleaving (u, A, ✓ # v)})
            | ✓ ⇒
    (case f of ev b ⇒   if b ∈ A then {}
                       else {ev b # t| t. t ∈ setinterleaving (✓ # u, A, v)}
             | ✓ ⇒ {✓ # t |t. t ∈ setinterleaving (u, A, v)}))›
  by (cases e; cases f) simp_all


lemmas setinterleaving_simps =
  Cons_setinterleaving_Nil Nil_setinterleaving_Cons Cons_setinterleaving_Cons 



abbreviation setinterleaves ::
  ‹['a trace, 'a trace, 'a trace, 'a set] ⇒ bool›
  (‹(_ /(setinterleaves)/ '(()'(_, _')(), _'))› [63,0,0,0] 64)
  where ‹t setinterleaves ((u, v), A) ≡ t ∈ setinterleaving (u, A, v)›




lemma tickFree_setinterleaves_iff :
  ‹t setinterleaves ((u, v), A) ⟹ tF t ⟷ tF u ∧ tF v›
  by (induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
    (auto split: if_split_asm)

lemma setinterleaves_tickFree_imp :
  ‹tF u ∨ tF v ⟹ t setinterleaves ((u, v), A) ⟹ tF t ∧ tF u ∧ tF v›
  by (elim disjE; induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
    (auto split: if_split_asm)



lemma setinterleaves_NilL_iff :
  ‹t setinterleaves (([], v), A) ⟷
   tF v ∧ set v ∩ ev ` A = {} ∧ t = map ev (map of_ev v)›
  by (induct ‹([] :: 'a trace, A, v)› arbitrary: t v rule: setinterleaving_induct)
    (auto split: if_split_asm)

lemma setinterleaves_NilR_iff :
  ‹t setinterleaves ((u, []), A) ⟷
   tF u ∧ set u ∩ ev ` A = {} ∧ t = map ev (map of_ev u)›
  by (induct ‹(u, A, [] :: 'a trace)›
      arbitrary: t u rule: setinterleaving_induct)
    (auto split: if_split_asm)

lemma Nil_setinterleaves :
  ‹[] setinterleaves ((u, v), A) ⟹ u = [] ∧ v = []›
  by (induct ‹(u, A, v)› arbitrary: u v rule: setinterleaving_induct)
    (simp_all split: if_split_asm)


lemma front_tickFree_setinterleaves_iff :
  ‹t setinterleaves ((u, v), A) ⟹ ftF t ⟷ ftF u ∧ ftF v›
proof (induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
  case (tick_setinterleaving_tick u v) thus ?case
    by (simp add: split: if_split_asm)
      (metis Nil_setinterleaves Nil_setinterleaving_Nil front_tickFree_Cons_iff singletonD)
qed (simp add: setinterleaves_NilL_iff setinterleaves_NilR_iff split: if_split_asm;
    metis event.simps(3) front_tickFree_Cons_iff front_tickFree_Nil)+


lemma setinterleaves_snoc_notinL :
  ‹t setinterleaves ((u, v), A) ⟹ a ∉ A ⟹
   t @ [ev a] setinterleaves ((u @ [ev a], v), A)›
  by (induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
    (auto split: if_split_asm)

lemma setinterleaves_snoc_notinR :
  ‹t setinterleaves ((u, v), A) ⟹ a ∉ A ⟹
   t @ [ev a] setinterleaves ((u, v @ [ev a]), A)›
  by (induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
    (auto split: if_split_asm)

lemma setinterleaves_snoc_inside :
  ‹t setinterleaves ((u, v), A) ⟹ a ∈ A ⟹
   t @ [ev a] setinterleaves ((u @ [ev a], v @ [ev a]), A)›
  by (induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
    (auto split: if_split_asm)


lemma setinterleaves_snoc_tick :
  ‹t setinterleaves ((u, v), A) ⟹ t @ [✓] setinterleaves ((u @ [✓], v @ [✓]), A)›
  by (induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
    (auto split: if_split_asm)


lemma Cons_tick_setinterleavesE :
  ‹✓ # t setinterleaves ((u, v), A) ⟹
   (⋀u' v' r s. ⟦u = ✓ # u'; v = ✓ # v'; t setinterleaves ((u', v'), A)⟧ ⟹ thesis) ⟹ thesis›
  by (induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
    (simp_all split: if_split_asm)

lemma Cons_ev_setinterleavesE :
  ‹ev a # t setinterleaves ((u, v), A) ⟹
   (⋀u'. a ∉ A ⟹ u = ev a # u' ⟹ t setinterleaves ((u', v), A) ⟹ thesis) ⟹
   (⋀v'. a ∉ A ⟹ v = ev a # v' ⟹ t setinterleaves ((u, v'), A) ⟹ thesis) ⟹
   (⋀u' v'. a ∈ A ⟹ u = ev a # u' ⟹ v = ev a # v' ⟹
             t setinterleaves ((u', v'), A) ⟹ thesis) ⟹ thesis›
proof (induct ‹(u, A, v)› arbitrary: u v t rule: setinterleaving_induct)
  case Nil_setinterleaving_Nil thus ?case by simp
next
  case (ev_setinterleaving_Nil b u)
  from ev_setinterleaving_Nil.prems(1) show ?case
    by (simp add: ev_setinterleaving_Nil.prems(2) split: if_split_asm)
next
  case (tick_setinterleaving_Nil r u) thus ?case by simp
next
  case (Nil_setinterleaving_ev c v)
  from Nil_setinterleaving_ev.prems(1) show ?case
    by (simp add: Nil_setinterleaving_ev.prems(3) split: if_split_asm)
next
  case (Nil_setinterleaving_tick s v) thus ?case by simp
next
  case (ev_setinterleaving_ev b u c v)
  from ev_setinterleaving_ev.prems(1) show ?case
    by (simp add: ev_setinterleaving_ev.prems(2, 3, 4) split: if_split_asm)
      (use ev_setinterleaving_ev.prems(2, 3) in presburger)
next
  case (ev_setinterleaving_tick b u s v)
  from ev_setinterleaving_tick.prems(1) show ?case
    by (simp add: ev_setinterleaving_tick.prems(2) split: if_split_asm)
next
  case (tick_setinterleaving_ev r u c v)
  from tick_setinterleaving_ev.prems(1) show ?case
    by (simp add: tick_setinterleaving_ev.prems(3) split: if_split_asm)
next
  case (tick_setinterleaving_tick u v) thus ?case by simp
qed


lemma rev_setinterleaves_rev_rev_iff :
  ‹rev t setinterleaves ((rev u, rev v), A)
   ⟷ t setinterleaves ((u, v), A)›
proof (rule iffI)
  show ‹t setinterleaves ((u, v), A) ⟹
        rev t setinterleaves ((rev u, rev v), A)› for t u v
    by (induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
      (auto simp add: setinterleaves_snoc_notinL setinterleaves_snoc_notinR
        setinterleaves_snoc_inside setinterleaves_snoc_tick split: if_split_asm)
  from this[of ‹rev t› ‹rev u› ‹rev v›, simplified]
  show ‹rev t setinterleaves ((rev u, rev v), A) ⟹
        t setinterleaves ((u, v), A)› .
qed


lemma setinterleaves_preserves_ev_notin_set :
  ‹⟦ev a ∉ set u; ev a ∉ set v; t setinterleaves ((u, v), A)⟧ ⟹ ev a ∉ set t›
  by (induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
    (auto split: if_split_asm)



lemma setinterleaves_preserves_ev_inside_set :
  ‹⟦ev a ∈ set u; ev a ∈ set v; t setinterleaves ((u, v), A)⟧ ⟹ ev a ∈ set t›
proof (induct ‹(u, A, v)› arbitrary: t u v rule: setinterleaving_induct)
  case Nil_setinterleaving_Nil
  then show ?case by simp
next
  case (ev_setinterleaving_Nil a u)
  then show ?case by simp
next
  case (tick_setinterleaving_Nil u)
  then show ?case by simp
next
  case (Nil_setinterleaving_ev b v)
  then show ?case by simp
next
  case (Nil_setinterleaving_tick v)
  then show ?case by simp
next
  case (ev_setinterleaving_ev a u b v)
  from ev_setinterleaving_ev.prems show ?case
    by (simp_all split: if_split_asm)
      (insert ev_setinterleaving_ev.hyps; metis list.set_intros(1,2))+
next
  case (ev_setinterleaving_tick a u v)
  then show ?case by (auto split: if_split_asm)
next
  case (tick_setinterleaving_ev u b v)
  then show ?case by (auto split: if_split_asm)
next
  case (tick_setinterleaving_tick u v)
  then show ?case by auto
qed


lemma ev_notin_both_sets_imp_empty_setinterleaving :
  ‹⟦ev a ∈ set u ∧ ev a ∉ set v ∨ ev a ∉ set u ∧ ev a ∈ set v; a ∈ A⟧ ⟹
   setinterleaving (u, A, v) = {}›
  by (induct ‹(u, A, v)› arbitrary: u v rule: setinterleaving_induct)
    (simp_all, safe, auto)


lemma append_setinterleaves_imp :
  ‹t setinterleaves ((u, v), A) ⟹ t' ≤ t ⟹
   ∃u' ≤ u. ∃v' ≤ v. t' setinterleaves ((u', v'), A)›
proof (induct ‹(u, A, v)› arbitrary: t u v t' rule: setinterleaving_induct)
  case Nil_setinterleaving_Nil thus ?case by auto
next
  case (ev_setinterleaving_Nil a u)
  from ev_setinterleaving_Nil.prems
  obtain w w' where ‹a ∉ A› ‹t = ev a # w› ‹t' = [] ∨ t' = ev a # w'›
    ‹w' ≤ w› ‹w setinterleaves ((u, []), A)›
    by (simp split: if_split_asm) (metis (no_types) Prefix_Order.prefix_Cons Nil_prefix)
  from ‹t' = [] ∨ t' = ev a # w'› show ?case
  proof (elim disjE)
    show ‹t' = [] ⟹ ?case› by auto
  next
    assume ‹t' = ev a # w'›
    from ev_setinterleaving_Nil.hyps[OF ‹a ∉ A› ‹w setinterleaves ((u, []), A)› ‹w' ≤ w›]
    obtain u' v' where ‹u' ≤ u ∧ v' ≤ [] ∧ w' setinterleaves ((u', v'), A)› by blast
    hence ‹ev a # u' ≤ ev a # u ∧ v' ≤ [] ∧ t' setinterleaves ((ev a # u', v'), A)›
      by (auto simp add: ‹a ∉ A› ‹t' = ev a # w'›)
    thus ?case by blast
  qed
next
  case (tick_setinterleaving_Nil r u) thus ?case by simp
next
  case (Nil_setinterleaving_ev b v)
  from Nil_setinterleaving_ev.prems
  obtain w w' where ‹b ∉ A› ‹t = ev b # w› ‹t' = [] ∨ t' = ev b # w'›
    ‹w' ≤ w› ‹w setinterleaves (([], v), A)›
    by (simp split: if_split_asm) (metis (no_types) Prefix_Order.prefix_Cons Nil_prefix)
  from ‹t' = [] ∨ t' = ev b # w'› show ?case
  proof (elim disjE)
    show ‹t' = [] ⟹ ?case› by auto
  next
    assume ‹t' = ev b # w'›
    from Nil_setinterleaving_ev.hyps[OF ‹b ∉ A› ‹w setinterleaves (([], v), A)› ‹w' ≤ w›]
    obtain u' v' where ‹u' ≤ [] ∧ v' ≤ v ∧ w' setinterleaves ((u', v'), A)› by blast
    hence ‹u' ≤ [] ∧ ev b # v' ≤ ev b # v ∧ t' setinterleaves ((u', ev b # v'), A)›
      by (auto simp add: ‹b ∉ A› ‹t' = ev b # w'›)
    thus ?case by blast
  qed
next
  case (Nil_setinterleaving_tick s v) thus ?case by simp
next
  case (ev_setinterleaving_ev a u b v)
  from ev_setinterleaving_ev.prems
  consider ‹t' = []›
    |      (both_in)   w w' where ‹a ∈ A› ‹b ∈ A› ‹a = b› ‹t = ev a # w› ‹t' = ev a # w'›
      ‹w setinterleaves ((u, v), A)› ‹w' ≤ w›
    |      (inR_mvL)   w w' where ‹a ∉ A› ‹b ∈ A› ‹t = ev a # w› ‹t' = ev a # w'›
      ‹w setinterleaves ((u, ev b # v), A)› ‹w' ≤ w›
    |      (inL_mvR)   w w' where ‹a ∈ A› ‹b ∉ A› ‹t = ev b # w› ‹t' = ev b # w'›
      ‹w setinterleaves ((ev a # u, v), A)› ‹w' ≤ w›
    |      (notin_mvL) w w' where ‹a ∉ A› ‹b ∉ A› ‹t = ev a # w› ‹t' = ev a # w'›
      ‹w setinterleaves ((u, ev b # v), A)› ‹w' ≤ w›
    |      (notin_mvR) w w' where ‹a ∉ A› ‹b ∉ A› ‹t = ev b # w› ‹t' = ev b # w'›
      ‹w setinterleaves ((ev a # u, v), A)› ‹w' ≤ w›
    by (cases t') (auto split: if_split_asm)
  thus ?case
  proof cases
    from Nil_setinterleaving_Nil show ‹t' = [] ⟹ ?thesis› by blast
  next
    case both_in
    from ev_setinterleaving_ev(1)[OF both_in(1-3, 6-7)]
    obtain u' v' where ‹u' ≤ u ∧ v' ≤ v ∧ w' setinterleaves ((u', v'), A)› by blast
    hence ‹ev a # u' ≤ ev a # u ∧ ev b # v' ≤ ev b # v ∧ t' setinterleaves ((ev a # u', ev b # v'), A)›
      by (auto simp add: both_in(2, 3) ‹t' = ev a # w'›)
    thus ?thesis by blast
  next
    case inR_mvL
    from ev_setinterleaving_ev(3)[OF inR_mvL(1, 2, 5, 6)]
    obtain u' v' where ‹u' ≤ u ∧ v' ≤ ev b # v ∧ w' setinterleaves ((u', v'), A)› by blast
    hence ‹ev a # u' ≤ ev a # u ∧ v' ≤ ev b # v ∧ t' setinterleaves ((ev a # u', v'), A)›
      by (cases v') (auto simp add: inR_mvL(1, 4))
    thus ?thesis by blast
  next
    case inL_mvR
    from ev_setinterleaving_ev(2)[OF inL_mvR(1, 2, 5, 6)]
    obtain u' v' where ‹u' ≤ ev a # u ∧ v' ≤ v ∧ w' setinterleaves ((u', v'), A)› by blast
    hence ‹u' ≤ ev a # u ∧ ev b # v' ≤ ev b # v ∧ t' setinterleaves ((u', ev b # v'), A)›
      by (cases u') (auto simp add: inL_mvR(2, 4))
    thus ?thesis by blast
  next
    case notin_mvL
    from ev_setinterleaving_ev(4)[OF notin_mvL(1, 2, 5, 6)]
    obtain u' v' where ‹u' ≤ u ∧ v' ≤ ev b # v ∧ w' setinterleaves ((u', v'), A)› by blast
    hence ‹ev a # u' ≤ ev a # u ∧ v' ≤ ev b # v ∧ t' setinterleaves ((ev a # u', v'), A)›
      by (cases v') (auto simp add: notin_mvL(1, 4))
    thus ?thesis by blast
  next
    case notin_mvR
    from ev_setinterleaving_ev(5)[OF notin_mvR(1, 2, 5, 6)]
    obtain u' v' where ‹u' ≤ ev a # u ∧ v' ≤ v ∧ w' setinterleaves ((u', v'), A)› by blast
    hence ‹u' ≤ ev a # u ∧ ev b # v' ≤ ev b # v ∧ t' setinterleaves ((u', ev b # v'), A)›
      by (cases u') (auto simp add: notin_mvR(2, 4))
    thus ?thesis by blast
  qed
next
  case (ev_setinterleaving_tick a u v)
  from ev_setinterleaving_tick.prems
  obtain w w' where ‹a ∉ A› ‹t = ev a # w› ‹t' = [] ∨ t' = ev a # w'›
    ‹w' ≤ w› ‹w setinterleaves ((u, ✓ # v), A)›
    by (simp split: if_split_asm) (metis (no_types) Prefix_Order.prefix_Cons Nil_prefix)
  from ‹t' = [] ∨ t' = ev a # w'› show ?case
  proof (elim disjE)
    from Nil_setinterleaving_Nil show ‹t' = [] ⟹ ?case› by blast
  next
    assume ‹t' = ev a # w'›
    from ev_setinterleaving_tick.hyps[OF ‹a ∉ A› ‹w setinterleaves ((u, ✓ # v), A)› ‹w' ≤ w›]
    obtain u' v' where ‹u' ≤ u ∧ v' ≤ ✓ # v ∧ w' setinterleaves ((u', v'), A)› by blast
    hence ‹ev a # u' ≤ ev a # u ∧ v' ≤ ✓ # v ∧ t' setinterleaves ((ev a # u', v'), A)›
      by (cases v') (simp_all add: ‹a ∉ A› ‹t' = ev a # w'›)
    thus ?case by blast
  qed
next
  case (tick_setinterleaving_ev u b v)
  from tick_setinterleaving_ev.prems
  obtain w w' where ‹b ∉ A› ‹t = ev b # w› ‹t' = [] ∨ t' = ev b # w'›
    ‹w' ≤ w› ‹w setinterleaves ((✓ # u, v), A)›
    by (simp split: if_split_asm) (metis (no_types) Prefix_Order.prefix_Cons Nil_prefix)
  from ‹t' = [] ∨ t' = ev b # w'› show ?case
  proof (elim disjE)
    from Nil_setinterleaving_Nil show ‹t' = [] ⟹ ?case› by blast
  next
    assume ‹t' = ev b # w'›
    from tick_setinterleaving_ev.hyps[OF ‹b ∉ A› ‹w setinterleaves ((✓ # u, v), A)› ‹w' ≤ w›]
    obtain u' v' where ‹u' ≤ ✓ # u ∧ v' ≤ v ∧ w' setinterleaves ((u', v'), A)› by blast
    hence ‹u' ≤ ✓ # u ∧ ev b # v' ≤ ev b # v ∧ t' setinterleaves ((u', ev b # v'), A)›
      by (cases u') (simp_all add: ‹b ∉ A› ‹t' = ev b # w'›)
    thus ?case by blast
  qed
next
  case (tick_setinterleaving_tick u v)
  from tick_setinterleaving_tick.prems obtain w w'
    where ‹t = ✓ # w› ‹t' = [] ∨ t' = ✓ # w'›
      ‹w' ≤ w› ‹w setinterleaves ((u, v), A)›
    by (cases t') (auto split: option.split_asm)
  from ‹t' = [] ∨ t' = ✓ # w'› show ?case
  proof (elim disjE)
    from Nil_setinterleaving_Nil show ‹t' = [] ⟹ ?case› by blast
  next
    assume ‹t' = ✓ # w'›
    from tick_setinterleaving_tick.hyps
      [OF ‹w setinterleaves ((u, v), A)› ‹w' ≤ w›]
    obtain u' v' where ‹u' ≤ u ∧ v' ≤ v ∧ w' setinterleaves ((u', v'), A)› by blast
    hence ‹✓ # u' ≤ ✓ # u ∧ ✓ # v' ≤ ✓ # v ∧
           t' setinterleaves ((✓ # u', ✓ # v'), A)›
      by (simp add: ‹t' = ✓ # w'›)
    thus ?case by blast
  qed
qed



lift_definition Sync :: ‹'a process ⇒ 'a set ⇒ 'a process ⇒ 'a process›
  (‹(3(_ ⟦_⟧/ _))› [70, 0, 71] 70)
  is ‹λP A Q. {t. ∃t_P t_Q. t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒯 Q ∧ t setinterleaves ((t_P, t_Q), A)}›
proof -
  show ‹?thesis P A Q› (is ‹is_process ?t›) for P A Q
  proof (unfold is_process_def, intro conjI allI impI)
    from Nil_elem_T Nil_setinterleaving_Nil show ‹[] ∈ ?t› by blast
  next
    fix t assume ‹t ∈ ?t›
    then obtain t_P t_Q where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
      ‹t setinterleaves ((t_P, t_Q), A)› by blast
    from ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› front_tickFree_T
    have ‹ftF t_P› ‹ftF t_Q› by auto
    with ‹t setinterleaves ((t_P, t_Q), A)›
    show ‹ftF t› by (simp add: front_tickFree_setinterleaves_iff)
  next
    fix t u assume ‹t @ u ∈ ?t›
    then obtain t_P t_Q where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
      ‹t @ u setinterleaves ((t_P, t_Q), A)› by blast
    from this(3) obtain t_P' t_P'' t_Q' t_Q''
      where ‹t_P = t_P' @ t_P''› ‹t_Q = t_Q' @ t_Q''›
        ‹t setinterleaves ((t_P', t_Q'), A)›
      by (meson Prefix_Order.prefixE Prefix_Order.prefixI append_setinterleaves_imp)
    from ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› this(1, 2) have ‹t_P' ∈ 𝒯 P› ‹t_Q' ∈ 𝒯 Q›
      by (auto intro: T_dw_closed)
    with ‹t setinterleaves ((t_P', t_Q'), A)› show ‹t ∈ ?t› by blast
  qed
qed

lemma T_Sync :
  ‹𝒯 (P ⟦A⟧ Q) = {t. ∃t_P t_Q. t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒯 Q ∧ t setinterleaves ((t_P, t_Q), A)}›
  by (simp add: Sync.rep_eq)


lift_definition Interrupt :: ‹'a process ⇒ 'a process ⇒ 'a process› (infixl ‹△› 81)
  is ‹λP Q. 𝒯 P ∪ {t @ u |t u. t ∈ 𝒯 P ∧ tF t ∧ u ∈ 𝒯 Q}›
proof -
  show ‹?thesis P Q› (is ‹is_process ?t›) for P Q
  proof (unfold is_process_def, intro conjI allI impI)
    show ‹[] ∈ ?t› by (simp add: Nil_elem_T)
  next
    show ‹t ∈ ?t ⟹ ftF t› for t
      by (auto simp add: front_tickFree_append_iff intro: front_tickFree_T)
  next
    show ‹t @ u ∈ ?t ⟹ t ∈ ?t› for t u
      by (auto simp add: append_eq_append_conv2 intro: T_dw_closed)
  qed
qed





subsection ‹Constructiveness›

lemma restriction_process_Mprefix :
  ‹□a ∈ A → P a ↓ n = (case n of 0 ⇒ BOT | Suc m ⇒ □a∈A → (P a ↓ m))›
  by (auto simp add: process_eq_spec T_restriction_process T_Mprefix T_BOT
      Nil_elem_T nat.case_eq_if front_tickFree_Cons_iff front_tickFree_T)
    (metis Cons_eq_append_conv Suc_length_conv event.distinct(1) length_greater_0_conv
      list.size(3) nat.exhaust_sel tickFree_Cons_iff)


lemma constructive_Mprefix [simp] :
  ‹constructive (λb. □a∈A → f a b)› if ‹⋀a. a ∈ A ⟹ non_destructive (f a)›
proof -
  have ‹□a∈A → f a b = □a∈A → (if a ∈ A then f a b else STOP)› for b
    by (auto simp add: process_eq_spec T_Mprefix)
  moreover have ‹constructive (λb. □a∈A → (if a ∈ A then f a b else STOP))›
  proof (rule constructive_comp_non_destructive[of ‹λP. □a∈A → P a›])
    show ‹constructive (λP. □a∈A → P a)›
      by (rule constructiveI) (simp add: restriction_process_Mprefix restriction_fun_def)
  next
    show ‹non_destructive (λb a. if a ∈ A then f a b else STOP)›
      by (simp add: non_destructive_fun_iff, intro allI non_destructive_if_then_else)
        (simp_all add: ‹⋀a. a ∈ A ⟹ non_destructive (f a)› non_destructiveI)
  qed
  ultimately show ‹constructive (λb. □a∈A → f a b)› by simp
qed






subsection ‹Non Destructiveness›

lemma non_destructive_Choice [simp] :
  ‹non_destructive (λx. f x □ g x)›
  if ‹non_destructive f› ‹non_destructive g›
  for f g :: ‹'a :: restriction ⇒ 'b process›
proof -
  have * : ‹non_destructive (λ(P, Q). P □ Q :: 'b process)›
  proof (rule order_non_destructiveI, clarify)
    fix P Q P' Q' :: ‹'b process› and n
    assume ‹(P, Q) ↓ n = (P', Q') ↓ n›
    hence ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›
      by (simp_all add: restriction_prod_def)
    show ‹P □ Q ↓ n ≤ P' □ Q' ↓ n›
    proof (unfold less_eq_process_def, rule subsetI)
      show ‹t ∈ 𝒯 (P' □ Q' ↓ n) ⟹ t ∈ 𝒯 (P □ Q ↓ n)› for t
      proof (elim T_restriction_processE)
        show ‹t ∈ 𝒯 (P' □ Q') ⟹ length t ≤ n ⟹ t ∈ 𝒯 (P □ Q ↓ n)›
          by (simp add: T_restriction_process T_Choice)
            (metis (lifting) T_restriction_process T_restriction_processE
              Un_iff ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›)
      next
        show ‹⟦t = u @ v; u ∈ 𝒯 (P' □ Q'); length u = n; tF u; ftF v⟧
              ⟹ t ∈ 𝒯 (P □ Q ↓ n)› for u v
          by (simp add: T_restriction_process T_Choice)
            (metis (lifting) T_restriction_process T_restriction_processE Un_iff
              ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n› append.right_neutral append_eq_conv_conj)
      qed
    qed
  qed
  have ** : ‹non_destructive (λx. (f x, g x))›
    by (fact non_destructive_prod_codomain[OF that])
  from non_destructive_comp_non_destructive[OF * **, simplified]
  show ‹non_destructive (λx. f x □ g x)› .
qed


lemma restriction_process_GlobalChoice :
  ‹□a ∈ A. P a ↓ n = (if A = {} then case n of 0 ⇒ BOT | Suc m ⇒ STOP else □a ∈ A. (P a ↓ n))›
  by (auto simp add: process_eq_spec T_restriction_process T_GlobalChoice T_BOT T_STOP
      split: nat.split)


lemma non_destructive_GlobalChoice [simp] :
  ‹non_destructive (λb. □a∈A. f a b)› if ‹⋀a. a ∈ A ⟹ non_destructive (f a)›
proof -
  have ‹□a∈A. f a b = □a∈A. (if a ∈ A then f a b else STOP)› for b
    by (auto simp add: process_eq_spec T_GlobalChoice)
  moreover have ‹non_destructive (λb. □a∈A. (if a ∈ A then f a b else STOP))›
  proof (rule non_destructive_comp_non_destructive[of ‹λP. □a∈A. P a›])
    show ‹non_destructive (λP. □a∈A. P a)›
      by (rule non_destructiveI) (simp add: restriction_process_GlobalChoice restriction_fun_def)
  next
    show ‹non_destructive (λb a. if a ∈ A then f a b else STOP)›
      by (simp add: non_destructive_fun_iff, intro allI non_destructive_if_then_else)
        (simp_all add: ‹⋀a. a ∈ A ⟹ non_destructive (f a)› non_destructiveI)
  qed
  ultimately show ‹non_destructive (λb. □a∈A. f a b)› by simp
qed



subsection ‹Examples›

notepad begin
  fix A B :: ‹'b ⇒ 'a set›
  define P :: ‹'b ⇒ 'a process›
    where ‹P ≡ υ X. (λs. □ a ∈ A s → X s □ (□ b ∈ B s → X s))› (is ‹P ≡ υ X. ?f X›)
  have ‹P = ?f P›
    by (unfold P_def, subst restriction_fix_eq) simp_all

end


lemma ‹constructive (λX σ. □ e ∈ f σ → □ σ' ∈ g σ e. X σ')›
  by simp



lemma length_le_T_restriction_process_iff_T :
  ‹length t ≤ n ⟹ t ∈ 𝒯 (P ↓ n) ⟷ t ∈ 𝒯 P›
  by (auto simp add: T_restriction_process)



lemma restriction_adm_notin_T [simp] : ‹adm⇩↓ (λa. t ∉ 𝒯 a)›
proof (rule restriction_admI)
  fix σ and Σ assume ‹σ ─↓→ Σ› ‹⋀n. t ∉ 𝒯 (σ n)›
  from ‹σ ─↓→ Σ› obtain n0 where ‹∀k≥n0. Σ ↓ length t = σ k ↓ length t›
    by (blast dest: restriction_tendstoD)
  hence ‹∀k≥n0. 𝒯 (Σ ↓ length t) = 𝒯 (σ k ↓ length t)› by simp
  hence ‹∀k≥n0. t ∈ 𝒯 Σ ⟷ t ∈ 𝒯 (σ k)›
    by (metis dual_order.refl length_le_T_restriction_process_iff_T)
  with ‹⋀n. t ∉ 𝒯 (σ n)› show ‹t ∉ 𝒯 Σ› by blast
qed


lemma restriction_adm_in_T [simp] : ‹adm⇩↓ (λa. t ∈ 𝒯 a)›
proof (rule restriction_admI)
  fix σ and Σ assume ‹σ ─↓→ Σ› ‹⋀n. t ∈ 𝒯 (σ n)›
  from ‹σ ─↓→ Σ› obtain n0 where ‹∀k≥n0. Σ ↓ length t = σ k ↓ length t›
    by (blast dest: restriction_tendstoD)
  hence ‹∀k≥n0. 𝒯 (Σ ↓ length t) = 𝒯 (σ k ↓ length t)› by simp
  hence ‹∀k≥n0. t ∈ 𝒯 Σ ⟷ t ∈ 𝒯 (σ k)›
    by (metis dual_order.refl length_le_T_restriction_process_iff_T)
  with ‹⋀n. t ∈ 𝒯 (σ n)› show ‹t ∈ 𝒯 Σ› by blast
qed


(*<*)
end
  (*>*)