Theory Interrupt_Non_Destructive

(***********************************************************************************
 * 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 ‹Non Destructiveness of Interrupt›

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

subsection ‹Refinement›

lemma restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_Interrupt_FD :
  ‹P △ Q ↓ n ⊑⇩_F⇩_D (P ↓ n) △ (Q ↓ n)› (is ‹?lhs ⊑⇩_F⇩_D ?rhs›)
proof (unfold refine_defs, safe)  
  show * : ‹t ∈ 𝒟 ?lhs› if ‹t ∈ 𝒟 ?rhs› for t
  proof -
    from ‹t ∈ 𝒟 ?rhs› consider ‹t ∈ 𝒟 (P ↓ n)›
      | u v where ‹t = u @ v› ‹u ∈ 𝒯 (P ↓ n)› ‹tF u› ‹v ∈ 𝒟 (Q ↓ n)›
      by (simp add: D_Interrupt) blast
    thus ‹t ∈ 𝒟 ?lhs›
    proof cases
      show ‹t ∈ 𝒟 (P ↓ n) ⟹ t ∈ 𝒟 ?lhs›
        by (elim D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_kE) (auto simp add: D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k Interrupt_projs)
    next
      fix u v assume ‹t = u @ v› ‹u ∈ 𝒯 (P ↓ n)› ‹tF u› ‹v ∈ 𝒟 (Q ↓ n)›
      from ‹v ∈ 𝒟 (Q ↓ n)› show ‹t ∈ 𝒟 ?lhs›
      proof (elim D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_kE)
        from ‹t = u @ v› ‹u ∈ 𝒯 (P ↓ n)› ‹tF u› show ‹v ∈ 𝒟 Q ⟹ t ∈ 𝒟 ?lhs›
          by (auto simp add: restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_projs Interrupt_projs
              D_imp_front_tickFree front_tickFree_append)
      next
        fix w x assume ‹v = w @ x› ‹w ∈ 𝒯 Q› ‹length w = n› ‹tF w› ‹ftF x›
        from ‹u ∈ 𝒯 (P ↓ n)› consider ‹u ∈ 𝒟 (P ↓ n)› | ‹u ∈ 𝒯 P› ‹length u ≤ n›
          by (elim T_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_kE) (auto simp add: D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k)
        thus ‹t ∈ 𝒟 ?lhs›
        proof cases
          assume ‹u ∈ 𝒟 (P ↓ n)›
          with D_imp_front_tickFree ‹t = u @ v› ‹tF u› ‹v ∈ 𝒟 (Q ↓ n)› is_processT7
          have ‹t ∈ 𝒟 (P ↓ n)› by blast
          thus ‹t ∈ 𝒟 ?lhs› by (elim D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_kE)
              (auto simp add: D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k Interrupt_projs)
        next
          assume ‹u ∈ 𝒯 P› ‹length u ≤ n›
          hence ‹t = take n (u @ w) @ drop (n - length u) w @ x ∧
                 take n (u @ w) ∈ 𝒯 (P △ Q) ∧ length (take n (u @ w)) = n ∧
                 tF (take n (u @ w)) ∧ ftF (drop (n - length u) w @ x)›
            by (simp add: ‹t = u @ v› ‹v = w @ x› ‹length w = n› ‹tF u› T_Interrupt)
              (metis ‹ftF x› ‹tF u› ‹tF w› ‹w ∈ 𝒯 Q› append_take_drop_id
                front_tickFree_append is_processT3_TR_append tickFree_append_iff)
          with D_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k show ‹t ∈ 𝒟 ?lhs› by blast
        qed
      qed
    qed
  qed

  show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
    by (meson "*" is_processT8 mono_Interrupt proc_ord2a restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_approx_self)
qed



subsection ‹Non Destructiveness›

lemma Interrupt_non_destructive :
  ‹non_destructive (λ(P :: ('a, 'r) process⇩_p⇩_t⇩_i⇩_c⇩_k, Q). P △ Q)›
proof (rule order_non_destructiveI, clarify)
  fix P P' Q Q' :: ‹('a, 'r) process⇩_p⇩_t⇩_i⇩_c⇩_k› and n
  assume ‹(P, Q) ↓ n = (P', Q') ↓ n› ‹0 < n›
  hence ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›
    by (simp_all add: restriction_prod_def)
  show ‹P △ Q ↓ n ⊑⇩_F⇩_D P' △ Q' ↓ n›
  proof (rule leFD_restriction_process⇩_p⇩_t⇩_i⇩_c⇩_kI)
    show ‹t ∈ 𝒟 (P' △ Q') ⟹ t ∈ 𝒟 (P △ Q ↓ n)› for t
      by (metis (mono_tags, opaque_lifting) ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›
                in_mono le_ref1 mono_Interrupt_FD restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_FD_self
                restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_Interrupt_FD)
  next
    show ‹(s, X) ∈ ℱ (P' △ Q') ⟹ (s, X) ∈ ℱ (P △ Q ↓ n)› for s X
      by (metis (mono_tags, opaque_lifting) ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›
                failure_refine_def leFD_imp_leF mono_Interrupt_FD
                restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_FD_self
                restriction_process⇩_p⇩_t⇩_i⇩_c⇩_k_Interrupt_FD subset_iff)
  qed
qed



(*<*)
end
  (*>*)