Theory Process_Normalization_Properties

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         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
 ***********************************************************************************)


chapter ‹Advanced Properties of ProcOmata›

(*<*)
theory Process_Normalization_Properties
  imports Process_Normalization Deterministic_Processes
begin
(*>*)


section ‹Determinism of deterministic ProcOmata›

lemma deterministic_P⇩_S⇩_K⇩_I⇩_P⇩_S_d : ‹deterministic (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ)›
proof (induct A arbitrary: σ rule: P⇩_S⇩_K⇩_I⇩_P⇩_S_d_induct)
  show ‹adm⇩_↓ (λf. ∀x. deterministic (f x))› by simp
next
  show ‹deterministic STOP› by simp
next
  show ‹(⋀σ. deterministic (X σ)) ⟹
        deterministic (P⇩_S⇩_K⇩_I⇩_P⇩_S_d_step (ε A) (τ A) (ω A) X σ)› for X σ
    by (simp add: deterministic_Mprefix_iff split: option.split)
qed

corollary deterministic_P_d : ‹deterministic (P⟪A⟫⇩_d σ)›
  by (subst P⇩_S⇩_K⇩_I⇩_P⇩_S_d_updated_ω) (fact deterministic_P⇩_S⇩_K⇩_I⇩_P⇩_S_d)

corollary P⇩_S⇩_K⇩_I⇩_P⇩_S_d_FD_imp_eq_P⇩_S⇩_K⇩_I⇩_P⇩_S_d : ‹P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ ⊑⇩_F⇩_D P ⟹ P = P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ›
  using deterministic_iff_maximal_for_leFD[THEN iffD1, OF deterministic_P⇩_S⇩_K⇩_I⇩_P⇩_S_d] by fast

corollary P_d_FD_imp_eq_P_d : ‹P⟪A⟫⇩_d σ ⊑⇩_F⇩_D P ⟹ P = P⟪A⟫⇩_d σ›
  using deterministic_iff_maximal_for_leFD[THEN iffD1, OF deterministic_P_d] by fast



section ‹No Divergence for ProcOmata›

lemma div_free_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd : ‹𝒟 (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) = {}›
proof (induct A arbitrary: σ rule: P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_induct)
  have ‹adm⇩_↓ (λX. ∀σ t. t ∈ 𝒟 (X σ) ⟶ False)›
    by (intro restriction_adm_all restriction_adm_imp) simp_all
  thus ‹adm⇩_↓ (λX. ∀σ. 𝒟 (X σ) = {})› by simp
next
  from D_STOP show ‹𝒟 STOP = {}› .
next
  show ‹(⋀σ. 𝒟 (X σ) = {}) ⟹ 𝒟 (P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_step (ε A) (τ A) (ω A) X σ) = {}› for X σ
    by (simp add: D_Mprefix D_GlobalNdet D_SKIPS)
qed

corollary div_free_P⇩_S⇩_K⇩_I⇩_P⇩_S_d : ‹𝒟 (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) = {}›
  by (simp add: deterministic_P⇩_S⇩_K⇩_I⇩_P⇩_S_d deterministic_div_free)

corollary div_free_P_nd : ‹𝒟 (P⟪A⟫⇩_n⇩_d s) = {}›
  by (simp add: P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_updated_ω div_free_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd)

corollary div_free_P_d : ‹𝒟 (P⟪A⟫⇩_d s) = {}›
  by (simp add: deterministic_P_d deterministic_div_free)



section ‹Reachability and Path›

text ‹We first need a preliminary result on \<^const>‹ℛ⇩_n⇩_d›: a state \<^term>‹t› is reachable
      from a state \<^term>‹s› if and only if there exists a path between \<^term>‹s› and \<^term>‹t››

(* we may want to formalize the definition of a path, but not for the moment *)

lemma ℛ⇩_n⇩_d_iff_Ex_path:
  ‹σ' ∈ ℛ⇩_n⇩_d A σ ⟷ (∃path. path ≠ [] ∧ hd path = σ ∧ last path = σ' ∧
                            (∀i < length path - 1. ∃a. path ! Suc i ∈ τ A (path ! i) a))›
  (is ‹_ ⟷ (∃path. path ≠ [] ∧ ?rhs path σ σ')›)
proof (rule iffI)
  show ‹σ' ∈ ℛ⇩_n⇩_d A σ ⟹ ∃path. path ≠ [] ∧ ?rhs path σ σ'›
  proof (induct rule: ℛ⇩_n⇩_d.induct)
    case init
    have ‹[σ] ≠ [] ∧ ?rhs [σ] σ σ› by simp
    thus ?case ..
  next
    case (step σ' σ'' a)
    from this(2) obtain path where ‹path ≠ [] ∧ ?rhs path σ σ'› ..
    with step.hyps(3) have ‹path @ [σ''] ≠ [] ∧ ?rhs (path @ [σ'']) σ σ''›
      by (simp add: nth_append)
        (metis One_nat_def Suc_lessI diff_Suc_Suc diff_zero last_conv_nth)
    thus ?case ..
  qed
next
  assume ‹∃path. path ≠ [] ∧ ?rhs path σ σ'›
  then obtain path where ‹path ≠ []› ‹?rhs path σ σ'› by blast
  thus ‹σ' ∈ ℛ⇩_n⇩_d A σ›
  proof (induct path arbitrary: σ rule: list_nonempty_induct)
    case (single u)
    thus ?case using ℛ⇩_n⇩_d.init by fastforce
  next
    case (cons σ'' path)
    have ‹σ' ∈ ℛ⇩_n⇩_d A (hd path)›
      by (rule cons.hyps(2))
        (use cons.hyps(1) cons.prems in simp,
          metis Suc_pred length_greater_0_conv not_less_eq nth_Cons_Suc)
    moreover have ‹hd path ∈ ℛ⇩_n⇩_d A σ›
      using ℛ⇩_n⇩_d.init ℛ⇩_n⇩_d.step cons.hyps(1) cons.prems hd_conv_nth by fastforce
    ultimately show ?case by (fact ℛ⇩_n⇩_d_trans)
  qed
qed

lemma ℛ⇩_d_iff_Ex_path: 
  ‹σ' ∈ ℛ⇩_d A σ ⟷ (∃path. path ≠ [] ∧ hd path = σ ∧ last path = σ' ∧
                            (∀i < length path - 1. ∃a. Some (path ! Suc i) = τ A (path ! i) a))›
  by (subst ℛ⇩_n⇩_d_from_det_to_ndet[symmetric], subst ℛ⇩_n⇩_d_iff_Ex_path)
    (simp add: from_det_to_ndet_def split: option.split, metis option.inject)



section ‹Deadlock Freeness and ProcOmata›

lemma deadlock_free_P_nd_step_iff :
  ‹deadlock_free (P_nd_step (ε A) (τ A) X σ) ⟷ 
      ε A σ ≠ {} ∧ (∀a ∈ ε A σ. ∀σ' ∈ τ A σ a. deadlock_free (X σ'))›
  and deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P_nd_step_iff :
  ‹deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P_nd_step (ε A) (τ A) X σ) ⟷ 
      ε A σ ≠ {} ∧ (∀a ∈ ε A σ. ∀σ' ∈ τ A σ a. deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (X σ'))›
  and deadlock_free_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_step_iff :
  ‹deadlock_free (P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_step (ε A) (τ A) (ω A) X σ) ⟷
      σ ∉ ρ A ∧ ε A σ ≠ {} ∧ (∀a ∈ ε A σ. ∀σ' ∈ τ A σ a. deadlock_free (X σ'))›
  and deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_step_iff :
  ‹deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_step (ε A) (τ A) (ω A) X σ) ⟷
      σ ∈ ρ A ∨ ε A σ ≠ {} ∧ (∀a ∈ ε A σ. ∀σ' ∈ τ A σ a. deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (X σ'))›
  by (simp_all add: deadlock_free_Mprefix_iff deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_Mprefix_iff
      deadlock_free_GlobalNdet_iff deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_GlobalNdet_iff
      non_deadlock_free_SKIPS deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_SKIPS ε_simps ρ_simps)


lemma deadlock_free_P_d_step_iff :
  ‹deadlock_free (P_d_step (ε A) (τ A) X σ) ⟷ 
       ε A σ ≠ {} ∧ (∀a ∈ ε A σ. deadlock_free (X ⌈τ A σ a⌉))›
  and deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P_d_step_iff :
  ‹deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P_d_step (ε A) (τ A) X σ) ⟷ 
      ε A σ ≠ {} ∧ (∀a ∈ ε A σ. deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (X ⌈τ A σ a⌉))›
  and deadlock_free_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_step_iff:
  ‹deadlock_free (P⇩_S⇩_K⇩_I⇩_P⇩_S_d_step (ε A) (τ A) (ω A) X σ) ⟷
      σ ∉ ρ A ∧ ε A σ ≠ {} ∧ (∀a ∈ ε A σ. deadlock_free (X ⌈τ A σ a⌉))›
  and deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_step_iff:
  ‹deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P⇩_S⇩_K⇩_I⇩_P⇩_S_d_step (ε A) (τ A) (ω A) X σ) ⟷
      σ ∈ ρ A ∨ ε A σ ≠ {} ∧ (∀a ∈ ε A σ. deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (X ⌈τ A σ a⌉))›
  by (simp_all add: deadlock_free_Mprefix_iff deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_Mprefix_iff
      non_deadlock_free_SKIP deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_SKIP ρ_simps
      split: option.split)


lemma deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd :
  ‹(⋀σ'. σ' ∈ ℛ⇩_n⇩_d A σ ⟹ σ' ∈ ρ A ∨ ε A σ' ≠ {}) ⟹
   deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ)›
proof (induct A arbitrary: σ rule: P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_induct)
  case adm
  show ?case by (simp add: deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_def)  
next
  show ‹deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (SKIP undefined)›
    by (fact deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_SKIP)
next
  case (step X) thus ?case
    unfolding deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_step_iff
    by (meson ℛ⇩_n⇩_d.init ℛ⇩_n⇩_d.step ℛ⇩_n⇩_d_trans)
qed

lemma deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_d :
  ‹(⋀σ'. σ' ∈ ℛ⇩_d A σ ⟹ σ' ∈ ρ A ∨ ε A σ' ≠ {}) ⟹
   deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ)›
proof (induct A arbitrary: σ rule: P⇩_S⇩_K⇩_I⇩_P⇩_S_d_induct)
  case adm
  show ?case by (simp add: deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_def)  
next
  show ‹deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (SKIP undefined)›
    by (fact deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_SKIP)
next
  case (step X)
  thus ?case
    unfolding deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_step_iff
    by (simp add: ε_simps) (metis ℛ⇩_d.init ℛ⇩_d.step ℛ⇩_d_trans option.sel)
qed


lemma deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_iff :
  assumes ‹ρ_disjoint_ε A›
  shows ‹deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⟷ (∀σ' ∈ ℛ⇩_n⇩_d A σ. σ' ∈ ρ A ∨ ε A σ' ≠ {})›
proof (intro iffI ballI)
  have ‹σ' ∈ ℛ⇩_n⇩_d A σ ⟹ deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⟹
        (σ' ∈ ρ A ∨ ε A σ' ≠ {}) ∧ deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ')› for σ'
  proof (induct rule: ℛ⇩_n⇩_d.induct)
    case init
    thus ?case
      by (subst (asm) P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec)
        (auto simp add: deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_step_iff init)
  next
    case (step σ' σ'' a)
    from step.hyps(2)[OF step.prems] step.hyps(3) ρ_disjoint_εD[OF assms]
    show ?case
      by (subst (asm) P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec)
        (auto simp add: deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_step_iff ε_simps,
          metis (mono_tags, lifting) Mprefix_is_STOP_iff P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec_notin_ρ
          SKIPS_empty ε_simps(2) deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_SKIPS empty_Collect_eq empty_iff)
  qed
  thus ‹σ' ∈ ℛ⇩_n⇩_d A σ ⟹ deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⟹ σ' ∈ ρ A ∨ ε A σ' ≠ {}› for σ' ..
next
  show ‹∀σ'∈ℛ⇩_n⇩_d A σ. σ' ∈ ρ A ∨ ε A σ' ≠ {} ⟹ deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ)›
    by (simp add: deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd)
qed


lemma deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_iff :
  ‹ρ_disjoint_ε A ⟹
   deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) ⟷ (∀σ' ∈ ℛ⇩_d A σ. σ' ∈ ρ A ∨ ε A σ' ≠ {})›
  by (fold P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_from_det_to_ndet_is_P⇩_S⇩_K⇩_I⇩_P⇩_S_d, subst deadlock_free⇩_S⇩_K⇩_I⇩_P⇩_S_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_iff)
    (simp_all add: ρ_disjoint_ε_def ℛ⇩_n⇩_d_from_det_to_ndet)




lemma deadlock_free_P_nd :
  ‹(⋀σ'. σ' ∈ ℛ⇩_n⇩_d A σ ⟹ ε A σ' ≠ {}) ⟹ deadlock_free (P⟪A⟫⇩_n⇩_d σ)›
proof (induct A arbitrary: σ rule: P_nd_induct)
  case adm
  show ?case by (simp add: deadlock_free_def)  
next
  show ‹deadlock_free (DF UNIV)›
    by (simp add: deadlock_free_def)
next
  case (step X) thus ?case
    unfolding deadlock_free_P_nd_step_iff
    by (meson ℛ⇩_n⇩_d.init ℛ⇩_n⇩_d.step ℛ⇩_n⇩_d_trans)
qed

lemma deadlock_free_P_d :
  ‹(⋀σ'. σ' ∈ ℛ⇩_d A σ ⟹ ε A σ' ≠ {}) ⟹ deadlock_free (P⟪A⟫⇩_d σ)›
proof (induct A arbitrary: σ rule: P_d_induct)
  case adm
  show ?case by (simp add: deadlock_free_def)  
next
  show ‹deadlock_free (DF UNIV)›
    by (simp add: deadlock_free_def)
next
  case (step X) thus ?case
    unfolding deadlock_free_P_d_step_iff
    by (simp add: ε_simps)
      (metis ℛ⇩_d.init ℛ⇩_d.step ℛ⇩_d_trans option.sel)
qed


lemma deadlock_free_P_nd_iff:
  ‹deadlock_free (P⟪A⟫⇩_n⇩_d σ) ⟷ (∀σ' ∈ ℛ⇩_n⇩_d A σ. ε A σ' ≠ {})›
proof (intro iffI ballI)
  have ‹σ' ∈ ℛ⇩_n⇩_d A σ ⟹ deadlock_free (P⟪A⟫⇩_n⇩_d σ) ⟹
        (ε A σ' ≠ {}) ∧ deadlock_free (P⟪A⟫⇩_n⇩_d σ')› for σ'
  proof (induct rule: ℛ⇩_n⇩_d.induct)
    case init
    thus ?case
      by (subst (asm) P_nd_rec)
        (auto simp add: deadlock_free_P_nd_step_iff init)
  next
    case (step σ' σ'' a)
    from step.hyps(2)[OF step.prems] step.hyps(3)
    show ?case
      by (subst (asm) P_nd_rec, unfold deadlock_free_P_nd_step_iff)
        (simp add: ε_simps,
          metis (mono_tags, lifting) P_nd_rec ε_simps(2)
          deadlock_free_Mprefix_iff empty_Collect_eq empty_iff)
  qed
  thus ‹σ' ∈ ℛ⇩_n⇩_d A σ ⟹ deadlock_free (P⟪A⟫⇩_n⇩_d σ) ⟹ ε A σ' ≠ {}› for σ' ..
next
  show ‹∀σ'∈ℛ⇩_n⇩_d A σ. ε A σ' ≠ {} ⟹ deadlock_free (P⟪A⟫⇩_n⇩_d σ)›
    by (simp add: deadlock_free_P_nd)
qed



lemma deadlock_free_P_d_iff :
  ‹deadlock_free (P⟪A⟫⇩_d σ) ⟷ (∀σ' ∈ ℛ⇩_d A σ. ε A σ' ≠ {})›
  by (fold P_nd_from_det_to_ndet_is_P_d, unfold deadlock_free_P_nd_iff)
    (simp add: ℛ⇩_n⇩_d_from_det_to_ndet)



section ‹Events and Ticks of ProcOmata›

subsection ‹Events›

lemma events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset :
  ‹α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⊆ (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ε A σ')›
proof (rule subsetI)
  fix a assume ‹a ∈ α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ)›
  then obtain t where ‹t ≠ []› ‹t ∈ 𝒯 (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ)› ‹ev a ∈ set t› 
    by (metis empty_iff empty_set events_of_memD)
  thus ‹a ∈ (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ε A σ')›
  proof (induct t arbitrary: σ rule: list_nonempty_induct)
    case (single t⇩₀)
    thus ?case by (subst (asm) P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec)
        (auto simp add: T_SKIPS T_Mprefix ℛ⇩_n⇩_d.init split: if_split_asm)
  next
    case (cons t⇩₀ t)
    from cons.prems(1) obtain b
      where ‹b ∈ ε A σ› ‹t⇩₀ = ev b› ‹t ∈ 𝒯 (⊓σ' ∈ τ A σ b. P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ')›
      by (subst (asm) (3) P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec)
        (auto simp add: T_Mprefix T_GlobalNdet T_SKIPS cons.hyps(1) ε_simps split: if_split_asm)
    thus ?case
      by (simp add: T_GlobalNdet cons.hyps(1) split: if_split_asm)
        (metis (no_types, lifting) UN_iff ℛ⇩_n⇩_d.simps ℛ⇩_n⇩_d_trans cons.hyps(2)
          cons.prems(2) event⇩_p⇩_t⇩_i⇩_c⇩_k.inject(1) set_ConsD)
  qed
qed

corollary events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_subset :
  ‹α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) ⊆ (⋃σ' ∈ ℛ⇩_d A σ. ε A σ')›
  by (metis P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_from_det_to_ndet_is_P⇩_S⇩_K⇩_I⇩_P⇩_S_d ℛ⇩_n⇩_d_from_det_to_ndet
      det_ndet_conv_ε(1) events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset)


lemma events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd :
  ‹α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) = (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ε A σ')›
  if ρ_disjoint_ε : ‹ρ_disjoint_ε A›
proof (intro subset_antisym subsetI)
  show ‹a ∈ α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⟹ a ∈ ⋃ (ε A ` ℛ⇩_n⇩_d A σ)› for a
    by (meson events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset in_mono)
next
  fix a assume ‹a ∈ (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ε A σ')›
  then obtain σ' where a1: ‹σ' ∈ ℛ⇩_n⇩_d A σ› and a2: ‹a ∈ ε A σ'› by blast
  from a1[simplified ℛ⇩_n⇩_d_iff_Ex_path] obtain path
    where ‹path ≠ []› ‹hd path = σ ∧ last path = σ' ∧ 
           (∀i<length path - 1. ∃e. path ! Suc i ∈ τ A (path ! i) e)› by blast
  from this a2 show ‹a ∈ α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ)›
  proof (induct path arbitrary: σ rule: list_nonempty_induct)
    case (single p)
    with ρ_disjoint_ε[THEN ρ_disjoint_εD] show ?case
      by (subst P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec)
        (auto simp add: events_of_Mprefix events_of_SKIPS ρ_simps)
  next
    case (cons p path)
    from cons(3) obtain b where ‹b ∈ ε A σ› ‹hd path ∈ τ A σ b›
      by (auto simp add: ε_simps) (metis cons(1) empty_iff hd_conv_nth length_greater_0_conv nth_Cons_0)
    moreover have ‹a ∈ α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d (hd path))›
      using a2 cons.hyps(1, 2) cons.prems(1) less_diff_conv by fastforce
    ultimately show ?case
      using ρ_disjoint_ε[THEN ρ_disjoint_εD]
      by (subst P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec)
        (auto simp add: events_of_Mprefix events_of_GlobalNdet events_of_SKIPS ρ_simps)
  qed
qed

corollary events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d: ‹ρ_disjoint_ε A ⟹ α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) = ⋃ (ε A ` ℛ⇩_d A σ)›
  by (fold P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_from_det_to_ndet_is_P⇩_S⇩_K⇩_I⇩_P⇩_S_d, subst events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd)
    (simp_all add: ρ_disjoint_ε_def ℛ⇩_n⇩_d_from_det_to_ndet)



lemma events_of_P_nd: ‹α(P⟪A⟫⇩_n⇩_d σ) = ⋃ (ε A ` ℛ⇩_n⇩_d A σ)›
  by (unfold P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_updated_ω, subst events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd)
    (auto simp add: ρ_disjoint_ε_def ρ_simps ε_simps)


lemma events_of_P_d: ‹α(P⟪A⟫⇩_d σ) = ⋃ (ε A ` ℛ⇩_d A σ)›
  by (metis P_nd_from_det_to_ndet_is_P_d ℛ⇩_n⇩_d_from_det_to_ndet
      det_ndet_conv_ε(1) events_of_P_nd)



subsection ‹Strict Events›

corollary strict_events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset :
  ‹❙α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⊆ (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ε A σ')›
  by (meson events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset order_trans strict_events_of_subset_events_of)

corollary strict_events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_subset :
  ‹❙α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) ⊆ (⋃σ' ∈ ℛ⇩_d A σ. ε A σ')›
  by (meson events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_subset order_trans strict_events_of_subset_events_of)

lemma strict_events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd :
  ‹ρ_disjoint_ε A ⟹ ❙α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) = (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ε A σ')›
  by (metis div_free_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd events_of_is_strict_events_of_or_UNIV)

corollary strict_events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d:
  ‹ρ_disjoint_ε A ⟹ ❙α(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) = (⋃σ' ∈ ℛ⇩_d A σ. ε A σ')›
  by (metis div_free_P⇩_S⇩_K⇩_I⇩_P⇩_S_d events_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d events_of_is_strict_events_of_or_UNIV)

lemma strict_events_of_P_nd: ‹❙α(P⟪A⟫⇩_n⇩_d σ) = (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ε A σ')›
  by (metis div_free_P_nd events_of_P_nd events_of_is_strict_events_of_or_UNIV)

lemma strict_events_of_P_d: ‹❙α(P⟪A⟫⇩_d σ) = (⋃σ' ∈ ℛ⇩_d A σ. ε A σ')›
  by (metis div_free_P_d events_of_P_d events_of_is_strict_events_of_or_UNIV)



subsection ‹Ticks›

lemma ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset :
  ‹✓s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⊆ (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ω A σ')›
proof (rule subsetI)
  fix r assume ‹r ∈ ✓s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ)›
  then obtain t where ‹t @ [✓(r)] ∈ 𝒯 (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ)›
    by (blast dest: ticks_of_memD)
  thus ‹r ∈ (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ω A σ')›
  proof (induct t arbitrary: σ)
    case Nil thus ?case
      by (subst (asm) P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec)
        (auto simp add: T_SKIPS ℛ⇩_n⇩_d.init split: if_split_asm)
  next
    case (Cons t⇩₀ t)
    from Cons.prems(1) obtain b
      where ‹b ∈ ε A σ› ‹t⇩₀ = ev b› ‹t @ [✓(r)] ∈ 𝒯 (⊓σ' ∈ τ A σ b. P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ')›
      by (subst (asm) (3) P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec)
        (auto simp add: T_Mprefix T_GlobalNdet T_SKIPS Cons.hyps(1) ε_simps split: if_split_asm)
    thus ?case
      by (simp add: T_GlobalNdet Cons.hyps(1) split: if_split_asm)
        (metis ℛ⇩_n⇩_d.init[of σ A] UN_iff[of r ‹ω A› ‹ℛ⇩_n⇩_d A _›]
          ℛ⇩_n⇩_d_trans[of _ A _ σ] ℛ⇩_n⇩_d.step[of σ A σ _ b] Cons.hyps)
  qed
qed

corollary ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_subset :
  ‹✓s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) ⊆ {⌈ω A σ'⌉ |σ'. σ' ∈ ℛ⇩_d A σ ∧ ω A σ' ≠ ◇}›
proof (fold P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_from_det_to_ndet_is_P⇩_S⇩_K⇩_I⇩_P⇩_S_d,
    rule subset_trans[OF ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset])
  show ‹(⋃σ' ∈ ℛ⇩_n⇩_d ⟪A⟫⇩_d⇩_↪⇩_n⇩_d σ. ω ⟪A⟫⇩_d⇩_↪⇩_n⇩_d σ') ⊆ {⌈ω A σ'⌉ |σ'. σ' ∈ ℛ⇩_d A σ ∧ ω A σ' ≠ ◇}›
    by (simp add: ℛ⇩_n⇩_d_from_det_to_ndet subset_iff)
      (simp add: from_det_to_ndet_def split: option.split, metis option.sel)
qed


lemma ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd :
  ‹✓s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) = (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ω A σ')›
  if ρ_disjoint_ε : ‹ρ_disjoint_ε A›
proof (intro subset_antisym subsetI)
  show ‹r ∈ ✓s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⟹ r ∈ (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ω A σ')› for r
    by (meson in_mono ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset)
next
  fix r assume ‹r ∈ (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ω A σ')›
  then obtain σ' where a1: ‹σ' ∈ ℛ⇩_n⇩_d A σ› and a2: ‹r ∈ ω A σ'› by blast
  from a1[simplified ℛ⇩_n⇩_d_iff_Ex_path] obtain path
    where ‹path ≠ []› ‹hd path = σ ∧ last path = σ' ∧ 
           (∀i<length path - 1. ∃e. path ! Suc i ∈ τ A (path ! i) e)› by blast
  from this a2 show ‹r ∈ ✓s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ)›
  proof (induct path arbitrary: σ rule: list_nonempty_induct)
    case (single p)
    thus ?case
      by (subst P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec)
        (auto simp add: ticks_of_SKIPS)
  next
    case (cons p path)
    from cons(3) obtain b where ‹b ∈ ε A σ› ‹hd path ∈ τ A σ b›
      by (auto simp add: ε_simps) (metis cons(1) empty_iff hd_conv_nth length_greater_0_conv nth_Cons_0)
    moreover have ‹r ∈ ✓s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d (hd path))›
      using a2 cons.hyps(1, 2) cons.prems(1) less_diff_conv by fastforce
    ultimately show ?case
      using ρ_disjoint_ε[THEN ρ_disjoint_εD]
      by (subst P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_rec)
        (auto simp add: ticks_of_Mprefix ticks_of_GlobalNdet events_of_SKIPS ρ_simps)
  qed
qed

corollary ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d :
  ‹ρ_disjoint_ε A ⟹ ✓s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) = {⌈ω A σ'⌉ |σ'. σ' ∈ ℛ⇩_d A σ ∧ ω A σ' ≠ ◇}›
  by (fold P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_from_det_to_ndet_is_P⇩_S⇩_K⇩_I⇩_P⇩_S_d, subst ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd,
      simp_all add: ρ_disjoint_ε_def ℛ⇩_n⇩_d_from_det_to_ndet)
    (auto simp add: from_det_to_ndet_def split: option.split_asm, metis option.sel)


lemma ticks_of_P_nd : ‹✓s(P⟪A⟫⇩_n⇩_d σ) = {}›
  by (simp add: P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_updated_ω ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd)

lemma ticks_of_P_d: ‹✓s(P⟪A⟫⇩_d σ) = {}›
  by (metis P_nd_from_det_to_ndet_is_P_d ticks_of_P_nd)



lemma non_terminating_iff_empty_ticks_of :
  ‹non_terminating P ⟷ ✓s(P) = {}›
  by (simp add: non_terminating_is_right tickFree_traces_iff_empty_ticks_of)



corollary non_terminating_P_nd : ‹non_terminating (P⟪A⟫⇩_n⇩_d σ)›
  by (simp add: non_terminating_iff_empty_ticks_of ticks_of_P_nd)

corollary non_terminating_P_d : ‹non_terminating (P⟪A⟫⇩_d σ)›
  by (metis P_nd_from_det_to_ndet_is_P_d non_terminating_P_nd)

corollary non_terminating_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd :
  ‹ρ A ∩ ℛ⇩_n⇩_d A σ = {} ⟹ non_terminating (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ)›
  by (simp add: P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_empty_ρ_inter_ℛ⇩_n⇩_d non_terminating_P_nd)

corollary non_terminating_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_iff :
  ‹ρ_disjoint_ε A ⟹ non_terminating (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⟷ ρ A ∩ ℛ⇩_n⇩_d A σ = {}›
  by (auto simp add: non_terminating_iff_empty_ticks_of ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd ρ_simps)

corollary non_terminating_P⇩_S⇩_K⇩_I⇩_P⇩_S_d :
  ‹ρ A ∩ ℛ⇩_d A σ = {} ⟹ non_terminating (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ)›
  by (simp add: P⇩_S⇩_K⇩_I⇩_P⇩_S_d_empty_ρ_inter_ℛ⇩_d non_terminating_P_d)

corollary non_terminating_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_iff :
  ‹ρ_disjoint_ε A ⟹ non_terminating (P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) ⟷ ρ A ∩ ℛ⇩_d A σ = {}›
  by (auto simp add: non_terminating_iff_empty_ticks_of ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d ρ_simps)



subsection ‹Strict Ticks›

corollary strict_ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset :
  ‹❙✓❙s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⊆ (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ω A σ')›
  by (metis div_free_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset ticks_of_is_strict_ticks_of_or_UNIV)

corollary strict_ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_subset :
  ‹❙✓❙s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) ⊆ {⌈ω A σ'⌉ |σ'. σ' ∈ ℛ⇩_d A σ ∧ ω A σ' ≠ ◇}›
  by (metis (mono_tags, lifting) strict_ticks_of_subset_ticks_of subset_trans ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_subset)

lemma strict_ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd :
  ‹ρ_disjoint_ε A ⟹ ❙✓❙s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) = (⋃σ' ∈ ℛ⇩_n⇩_d A σ. ω A σ')›
  by (metis div_free_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd ticks_of_is_strict_ticks_of_or_UNIV)

corollary strict_ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d :
  ‹ρ_disjoint_ε A ⟹ ❙✓❙s(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) = {⌈ω A σ'⌉ |σ'. σ' ∈ ℛ⇩_d A σ ∧ ω A σ' ≠ ◇}›
  by (metis (mono_tags, lifting) div_free_P⇩_S⇩_K⇩_I⇩_P⇩_S_d ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d ticks_of_is_strict_ticks_of_or_UNIV)

lemma strict_ticks_of_P_nd: ‹❙✓❙s(P⟪A⟫⇩_n⇩_d σ) = {}›
  by (metis div_free_P_nd ticks_of_P_nd ticks_of_is_strict_ticks_of_or_UNIV)

lemma strict_ticks_of_P_d: ‹❙✓❙s(P⟪A⟫⇩_d σ) = {}›
  by (metis P_nd_from_det_to_ndet_is_P_d strict_ticks_of_P_nd)



subsection ‹Ticks length›

lemma is_ticks_length_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd :
  ‹⟦⋀σ' rs. σ' ∈ ℛ⇩_n⇩_d A σ ⟹ rs ∈ ω A σ' ⟹ length rs = n⟧
   ⟹ length⇩_✓⇘n⇙(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ)›
  by (auto simp add: is_ticks_length_def
      dest!: set_mp[OF strict_ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_subset])

lemma is_ticks_length_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd_iff :
  ‹ρ_disjoint_ε A ⟹
   length⇩_✓⇘n⇙(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_n⇩_d σ) ⟷ (∀σ' ∈ ℛ⇩_n⇩_d A σ. ∀rs ∈ ω A σ'. length rs = n)›
  by (simp add: is_ticks_length_def strict_ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_nd)

lemma is_ticks_length_P⇩_S⇩_K⇩_I⇩_P⇩_S_d :
  ‹⟦⋀σ'. σ' ∈ ℛ⇩_d A σ ⟹ ω A σ' ≠ ◇ ⟹ length ⌈ω A σ'⌉ = n⟧
   ⟹ length⇩_✓⇘n⇙(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ)›
  by (auto simp add: is_ticks_length_def
      dest!: set_mp[OF strict_ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_subset])

lemma is_ticks_length_P⇩_S⇩_K⇩_I⇩_P⇩_S_d_iff :
  ‹ρ_disjoint_ε A ⟹
   length⇩_✓⇘n⇙(P⇩_S⇩_K⇩_I⇩_P⇩_S⟪A⟫⇩_d σ) ⟷ (∀σ' ∈ ℛ⇩_d A σ. ω A σ' ≠ ◇ ⟶ length ⌈ω A σ'⌉ = n)›
  by (auto simp add: is_ticks_length_def strict_ticks_of_P⇩_S⇩_K⇩_I⇩_P⇩_S_d)



(*<*)
end
(*>*)