Theory CSP_Restriction_Adm

(***********************************************************************************
 * 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
 ***********************************************************************************)

section ‹Admissibility›

(*<*)
theory CSP_Restriction_Adm
  imports Process_Restriction_Space After_Operator_Non_Too_Destructive
    "HOL-CSP_OpSem.Operational_Semantics_Laws"
begin 
  (*>*)


named_theorems restriction_adm_processptick_simpset

subsection ‹Belonging›

lemma restriction_adm_in_D [restriction_adm_processptick_simpset] :
  ‹adm↓ (λx. t ∈ 𝒟 (f x))›
  and restriction_adm_notin_D [restriction_adm_processptick_simpset] :
  ‹adm↓ (λx. t ∉ 𝒟 (f x))›
  and restriction_adm_in_F [restriction_adm_processptick_simpset] :
  ‹adm↓ (λx. (t, X) ∈ ℱ (f x))›
  and restriction_adm_notin_F [restriction_adm_processptick_simpset] :
  ‹adm↓ (λx. (t, X) ∉ ℱ (f x))› if ‹cont↓ f›
for f :: ‹'b :: restriction ⇒ ('a, 'r) processptick›
proof (all ‹rule restriction_adm_subst[OF ‹cont↓ f›]›)
  have * : ‹σ ─↓→ Σ ⟹ ∃n0. ∀n ≥ n0. σ n ↓ Suc (length t) = Σ ↓ Suc (length t)›
    for σ and Σ :: ‹('a, 'r) processptick›
    by (metis restriction_tendstoD)

  show ‹adm↓ (λx. t ∈ 𝒟 x)› ‹adm↓ (λx. t ∉ 𝒟 x)›
    by (rule restriction_admI,
        metis (no_types) "*" D_restriction_processptick_Suc_length_iff_D dual_order.refl)+

  show ‹adm↓ (λx. (t, X) ∈ ℱ x)› ‹adm↓ (λx. (t, X) ∉ ℱ x)›
    by (rule restriction_admI,
        metis (no_types) "*" F_restriction_processptick_Suc_length_iff_F dual_order.refl)+
qed


corollary restriction_adm_in_T [restriction_adm_processptick_simpset] :
  ‹cont↓ f ⟹ adm↓ (λx. t ∈ 𝒯 (f x))›
  and restriction_adm_notin_T [restriction_adm_processptick_simpset] :
  ‹cont↓ f ⟹ adm↓ (λx. t ∉ 𝒯 (f x))›
  by (fact restriction_adm_in_F[of f t ‹{}›, simplified T_F_spec])
    (fact restriction_adm_notin_F[of f t ‹{}›, simplified T_F_spec])


corollary restriction_adm_in_initials [restriction_adm_processptick_simpset] :
  ‹cont↓ f ⟹ adm↓ (λx. e ∈ (f x)0)›
  and restriction_adm_notin_initials [restriction_adm_processptick_simpset] :
  ‹cont↓ f ⟹ adm↓ (λx. e ∉ (f x)0)›
  by (simp_all add: initials_def restriction_adm_in_T restriction_adm_notin_T)



subsection ‹Refining›

corollary restriction_adm_leF [restriction_adm_processptick_simpset] :
  ‹cont↓ f ⟹ cont↓ g ⟹ adm↓ (λx. f x ⊑F g x)›
  by (simp add: failure_refine_def subset_iff restriction_adm_processptick_simpset)

corollary restriction_adm_leD [restriction_adm_processptick_simpset] :
  ‹cont↓ f ⟹ cont↓ g ⟹ adm↓ (λx. f x ⊑D g x)› 
  by (simp add: divergence_refine_def subset_iff restriction_adm_processptick_simpset)

corollary restriction_adm_leT [restriction_adm_processptick_simpset] :
  ‹cont↓ f ⟹ cont↓ g ⟹ adm↓ (λx. f x ⊑T g x)›
  by (simp add: trace_refine_def subset_iff restriction_adm_processptick_simpset)

corollary restriction_adm_leFD [restriction_adm_processptick_simpset] :
  ‹cont↓ f ⟹ cont↓ g ⟹ adm↓ (λx. f x ⊑FD g x)›
  by (simp add: failure_divergence_refine_def restriction_adm_processptick_simpset)

corollary restriction_adm_leDT [restriction_adm_processptick_simpset] :
  ‹cont↓ f ⟹ cont↓ g ⟹ adm↓ (λx. f x ⊑DT g x)› 
  by (simp add: trace_divergence_refine_def restriction_adm_processptick_simpset)




subsubsection ‹Transitions›

lemma (in After) restriction_cont_After [restriction_adm_simpset] :
  ‹cont↓ (λx. f x after a)› if ‹cont↓ f› and ‹cont↓ Ψ›
  ― ‹We could imagine more precise assumptions, but is it useful?›
proof (rule restriction_cont_comp[OF _ ‹cont↓ f›])
  show ‹cont↓ (λP. P after a)›
  proof (rule restriction_contI)
    show ‹(λn. σ n after a) ─↓→ Σ after a› if ‹σ ─↓→ Σ› for σ Σ
    proof (rule restriction_tendstoI)
      fix n
      from ‹σ ─↓→ Σ› obtain n0
        where * : ‹∀k≥n0. Σ ↓ Suc n = σ k ↓ Suc n›
        by (blast dest: restriction_tendstoD)
      consider ‹ev a ∈ Σ0› ‹∀n≥Suc n0. ev a ∈ (σ n)0›
        | ‹ev a ∉ Σ0› ‹∀n≥Suc n0. ev a ∉ (σ n)0›
        by (metis "*" Suc_leD initials_restriction_processptick nat.distinct(1))
      thus ‹∃n0. ∀k≥n0. Σ after a ↓ n = σ k after a ↓ n›
      proof cases
        assume ‹ev a ∈ Σ0› ‹∀n≥Suc n0. ev a ∈ (σ n)0›
        hence ‹∀k≥Suc n0. Σ after a ↓ n = σ k after a ↓ n›
          by (metis "*" Suc_leD restriction_processptick_After)
        thus ‹∃n0. ∀k≥n0. Σ after a ↓ n = σ k after a ↓ n› ..
      next
        assume ‹ev a ∉ Σ0› ‹∀n≥Suc n0. ev a ∉ (σ n)0›
        hence ‹Σ after a = Ψ Σ a› ‹∀k≥Suc n0. σ k after a = Ψ (σ k) a›
          by (simp_all add: not_initial_After)
        moreover from ‹cont↓ Ψ›[THEN restriction_contD]
        obtain n1 where ‹∀k≥n1. Ψ Σ ↓ n = Ψ (σ k) ↓ n›
          by (blast intro: ‹σ ─↓→ Σ› dest: restriction_tendstoD)
        ultimately have ‹∀k≥max n1 (Suc n0). Σ after a ↓ n = σ k after a ↓ n›
          by simp (metis restriction_fun_def)
        thus ‹∃n0. ∀k≥n0. Σ after a ↓ n = σ k after a ↓ n› ..
      qed
    qed
  qed
qed

lemma (in AfterExt) restriction_cont_Aftertick [restriction_adm_simpset] :
  ‹cont↓ (λx. f x after✓ e)› if ‹cont↓ f› and ‹cont↓ Ψ› and ‹cont↓ Ω›
  ― ‹We could imagine more precise assumptions, but is it useful?›
proof (cases e)
  show ‹e = ev a ⟹ cont↓ (λx. f x after✓ e)› for a
    by (simp add: Aftertick_def restriction_cont_After ‹cont↓ f› ‹cont↓ Ψ›)
next
  fix r assume ‹e = ✓(r)›
  hence ‹(λx. f x after✓ e) = (λx. Ω (f x) r)› by (simp add: Aftertick_def)
  thus ‹cont↓ (λx. f x after✓ e)›
    by (metis restriction_cont_comp restriction_cont_fun_imp that(1,3))
qed

lemma (in AfterExt) restriction_cont_Aftertrace [restriction_adm_simpset] :
  ‹cont↓ (λx. f x after𝒯 t)› if ‹cont↓ f› and ‹cont↓ Ψ› and ‹cont↓ Ω›
  ― ‹We could imagine more precise assumptions, but is it useful?›
proof (rule restriction_cont_comp[OF _ ‹cont↓ f›])
  show ‹cont↓ (λP. P after𝒯 t)›
  proof (induct t)
    show ‹cont↓ (λP. P after𝒯 [])› by simp
  next
    fix e t assume ‹cont↓ (λP. P after𝒯 t)›
    show ‹cont↓ (λP. P after𝒯 (e # t))›
      by (simp, rule restriction_cont_comp[OF ‹cont↓ (λP. P after𝒯 t)›])
        (simp add: restriction_cont_Aftertick ‹cont↓ Ψ› ‹cont↓ Ω›)
  qed
qed


lemma (in OpSemTransitions) restriction_adm_weak_ev_trans [restriction_adm_processptick_simpset]:
  ― ‹Could be weakened to a continuity assumption on term‹Ψ›.›
  fixes f g :: ‹'b :: restriction ⇒ ('a, 'r) processptick›
  assumes τ_trans_restriction_adm:
    ‹⋀f g :: 'b ⇒ ('a, 'r) processptick. cont↓ f ⟹ cont↓ g ⟹ adm↓ (λx. f x ↝τ g x)›
    and ‹cont↓ f› and ‹cont↓ g› and ‹cont↓ Ψ› and ‹cont↓ Ω›
  shows ‹adm↓ (λx. f x ↝⇘e⇙ g x)›
proof (intro restriction_adm_conj)
  show ‹adm↓ (λx. ev e ∈ (f x)0)›
    by (simp add: ‹cont↓ f› restriction_adm_in_initials)
next
  show ‹adm↓ (λx. f x after✓ ev e ↝τ g x)›
  proof (rule τ_trans_restriction_adm[OF _ ‹cont↓ g›],
      rule restriction_cont_comp[OF _ ‹cont↓ f›])
    show ‹cont↓ (λx. x after✓ ev e)›
      by (simp add: ‹cont↓ Ψ› ‹cont↓ Ω› restriction_cont_Aftertick)
  qed
qed

lemma (in OpSemTransitions) restriction_adm_weak_tick_trans [restriction_adm_processptick_simpset]:
  fixes f g :: ‹'b :: restriction ⇒ ('a, 'r) processptick›
  assumes τ_trans_restriction_adm:
    ‹⋀f g :: 'b ⇒ ('a, 'r) processptick. cont↓ f ⟹ cont↓ g ⟹ adm↓ (λx. f x ↝τ g x)›
    and ‹cont↓ f› and ‹cont↓ g› and ‹cont↓ Ψ› and ‹cont↓ Ω›
  shows ‹adm↓ (λx. f x ↝✓⇘r⇙ (g x))›
proof (intro restriction_adm_conj)
  show ‹adm↓ (λx. ✓(r) ∈ (f x)0)›
    by (simp add: ‹cont↓ f› restriction_adm_in_initials)
next
  show ‹adm↓ (λx. f x after✓ ✓(r) ↝τ g x)›
  proof (rule τ_trans_restriction_adm[OF _ ‹cont↓ g›],
      rule restriction_cont_comp[OF _ ‹cont↓ f›])
    show ‹cont↓ (λx. x after✓ ✓(r))›
      by (simp add: ‹cont↓ Ψ› ‹cont↓ Ω› restriction_cont_Aftertick)
  qed
qed

lemma (in OpSemTransitions) restriction_adm_weak_trace_trans [restriction_adm_processptick_simpset]:
  fixes f g :: ‹'b :: restriction ⇒ ('a, 'r) processptick›
  assumes τ_trans_restriction_adm:
    ‹⋀f g :: 'b ⇒ ('a, 'r) processptick. cont↓ f ⟹ cont↓ g ⟹ adm↓ (λx. f x ↝τ g x)›
    and ‹cont↓ f› and ‹cont↓ g› and ‹cont↓ Ψ› and ‹cont↓ Ω›
  shows ‹adm↓ (λx. f x ↝* t (g x))›
proof (subst trace_trans_iff_T_and_Aftertrace_τ_trans, intro restriction_adm_conj)
  show ‹adm↓ (λx. t ∈ 𝒯 (f x))› by (simp add: ‹cont↓ f› restriction_adm_in_T)
next
  show ‹adm↓ (λx. f x after𝒯 t ↝τ g x)›
  proof (rule τ_trans_restriction_adm[OF _ ‹cont↓ g›])
    show ‹cont↓ (λx. f x after𝒯 t)›
      by (simp add: ‹cont↓ f› ‹cont↓ Ψ› ‹cont↓ Ω› restriction_cont_Aftertrace)
  qed
qed



declare restriction_adm_processptick_simpset [simp]


(*<*)
end
  (*>*)