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.CSPM_Laws"
begin
  (*>*)

subsection ‹Refinement›

lemma restriction_processptick_Interrupt_FD :
  ‹P △ Q ↓ n ⊑FD (P ↓ n) △ (Q ↓ n)› (is ‹?lhs ⊑FD ?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_processptickE) (auto simp add: D_restriction_processptick 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_processptickE)
        from ‹t = u @ v› ‹u ∈ 𝒯 (P ↓ n)› ‹tF u› show ‹v ∈ 𝒟 Q ⟹ t ∈ 𝒟 ?lhs›
          by (auto simp add: restriction_processptick_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_processptickE) (auto simp add: D_restriction_processptick)
        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_processptickE)
              (auto simp add: D_restriction_processptick 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_processptick 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_processptick_approx_self)
qed



subsection ‹Non Destructiveness›

lemma Interrupt_non_destructive :
  ‹non_destructive (λ(P :: ('a, 'r) processptick, Q). P △ Q)›
proof (rule order_non_destructiveI, clarify)
  fix P P' Q Q' :: ‹('a, 'r) processptick› 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)

  { let ?lhs = ‹P △ Q ↓ n›
    fix t u v assume ‹t = u @ v› ‹u ∈ 𝒯 (P' △ Q')› ‹length u = n› ‹tF u› ‹ftF v›
    from this(2) ‹tF u› obtain u1 u2
      where ‹u = u1 @ u2› ‹u1 ∈ 𝒯 P'› ‹tF u1› ‹u2 ∈ 𝒯 Q'› ‹tF u2›
      by (simp add: T_Interrupt)
        (metis append_Nil2 is_processT1_TR tickFree_append_iff)

    from ‹length u = n› ‹u = u1 @ u2›
    have ‹length u1 ≤ n› ‹length u2 ≤ n› by simp_all
    with ‹u1 ∈ 𝒯 P'› ‹P ↓ n = P' ↓ n› ‹u2 ∈ 𝒯 Q'› ‹Q ↓ n = Q' ↓ n›
    have ‹u1 ∈ 𝒯 P› ‹u2 ∈ 𝒯 Q›
      by (metis T_restriction_processptickI
          length_le_in_T_restriction_processptick)+
    with ‹tF u1› have ‹u ∈ 𝒯 (P △ Q)›
      by (auto simp add: ‹u = u1 @ u2› T_Interrupt)
    with ‹length u = n› ‹tF u› have ‹u ∈ 𝒟 ?lhs›
      by (simp add: D_restriction_processptickI)
    hence ‹t ∈ 𝒟 ?lhs› by (simp add: ‹ftF v› ‹t = u @ v› ‹tF u› is_processT7)
  } note * = this

  show ‹P △ Q ↓ n ⊑FD P' △ Q' ↓ n› (is ‹?lhs ⊑FD ?rhs›)
  proof (unfold refine_defs, safe)
    show div : ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    proof (elim D_restriction_processptickE)
      assume ‹t ∈ 𝒟 (P' △ Q')› ‹length t ≤ n›
      from this(1) consider ‹t ∈ 𝒟 P'›
        | (divR) t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒯 P'› ‹tF t1› ‹t2 ∈ 𝒟 Q'›
        unfolding D_Interrupt by blast
      thus ‹t ∈ 𝒟 ?lhs›
      proof cases
        assume ‹t ∈ 𝒟 P'›
        hence ‹ftF t› by (simp add: D_imp_front_tickFree)
        thus ‹t ∈ 𝒟 ?lhs›
        proof (elim front_tickFreeE)
          show ‹t ∈ 𝒟 ?lhs› if ‹tF t›
          proof (cases ‹length t = n›)
            assume ‹length t = n›
            from ‹P ↓ n = P' ↓ n› ‹t ∈ 𝒟 P'› ‹length t ≤ n› have ‹t ∈ 𝒯 P›
              by (metis D_T T_restriction_processptickI
                  length_le_in_T_restriction_processptick)
            with ‹tF t› ‹length t = n› front_tickFree_Nil show ‹t ∈ 𝒟 ?lhs›
              by (simp (no_asm) add: D_restriction_processptick T_Interrupt) blast
          next
            assume ‹length t ≠ n›
            with ‹length t ≤ n› have ‹length t < n› by simp
            with ‹P ↓ n = P' ↓ n› ‹t ∈ 𝒟 P'› have ‹t ∈ 𝒟 P›
              by (metis D_restriction_processptickI
                  length_less_in_D_restriction_processptick)
            thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_restriction_processptickI D_Interrupt)
          qed
        next
          fix t' r assume ‹t = t' @ [✓(r)]› ‹tF t'›
          with ‹t ∈ 𝒟 P'› ‹length t ≤ n›
          have ‹t' ∈ 𝒟 P'› ‹length t' < n› by (auto intro: is_processT9)
          with ‹P ↓ n = P' ↓ n› have ‹t' ∈ 𝒟 P›
            by (metis D_restriction_processptickI
                length_less_in_D_restriction_processptick)
          with ‹t = t' @ [✓(r)]› ‹tF t'› have ‹t ∈ 𝒟 P› by (simp add: is_processT7)
          thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_restriction_processptickI D_Interrupt)
        qed
      next
        fix u v assume ‹t = u @ v› ‹u ∈ 𝒯 P'› ‹tF u› ‹v ∈ 𝒟 Q'›
        from ‹t = u @ v› ‹length t ≤ n› have ‹length u ≤ n› by simp
        with ‹P ↓ n = P' ↓ n› ‹u ∈ 𝒯 P'› have ‹u ∈ 𝒯 P›
          by (metis T_restriction_processptickI length_le_in_T_restriction_processptick)
        show ‹t ∈ 𝒟 ?lhs›
        proof (cases ‹length v = n›)
          assume ‹length v = n›
          with ‹t = u @ v› ‹length t ≤ n› have ‹u = []› by simp
          from D_imp_front_tickFree ‹v ∈ 𝒟 Q'› have ‹ftF v› by blast
          thus ‹t ∈ 𝒟 ?lhs›
          proof (elim front_tickFreeE)
            assume ‹tF v›
            from ‹length v = n› ‹Q ↓ n = Q' ↓ n› ‹v ∈ 𝒟 Q'› have ‹v ∈ 𝒯 Q›
              by (metis D_T D_restriction_processptickI dual_order.refl
                  length_le_in_T_restriction_processptick)
            with ‹tF u› ‹u ∈ 𝒯 P› have ‹t ∈ 𝒯 (P △ Q)›
              by (auto simp add: ‹t = u @ v› T_Interrupt)
            with ‹length v = n› ‹t = u @ v› ‹tF v› ‹u = []› show ‹t ∈ 𝒟 ?lhs›
              by (simp add: D_restriction_processptickI)
          next
            fix v' r assume ‹v = v' @ [✓(r)]› ‹tF v'›
            with ‹v ∈ 𝒟 Q'› ‹length t ≤ n› ‹t = u @ v›
            have ‹v' ∈ 𝒟 Q'› ‹length v' < n› by (auto intro: is_processT9)
            with ‹Q ↓ n = Q' ↓ n› have ‹v' ∈ 𝒟 Q›
              by (metis D_restriction_processptickI
                  length_less_in_D_restriction_processptick)
            with ‹v = v' @ [✓(r)]› ‹tF v'› have ‹v ∈ 𝒟 Q› by (simp add: is_processT7)
            with ‹tF u› ‹u ∈ 𝒯 P› have ‹t ∈ 𝒟 (P △ Q)›
              by (auto simp add: ‹t = u @ v› D_Interrupt)
            thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_restriction_processptickI)
          qed
        next
          assume ‹length v ≠ n›
          with ‹length t ≤ n› ‹t = u @ v› have ‹length v < n› by simp
          with ‹Q ↓ n = Q' ↓ n› ‹v ∈ 𝒟 Q'› have ‹v ∈ 𝒟 Q›
            by (metis D_restriction_processptickI
                length_less_in_D_restriction_processptick)
          with ‹t = u @ v› ‹tF u› ‹u ∈ 𝒯 P› have ‹t ∈ 𝒟 (P △ Q)›
            by (auto simp add: D_Interrupt)
          thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_restriction_processptickI)
        qed
      qed
    next
      show ‹t = u @ v ⟹ u ∈ 𝒯 (P' △ Q') ⟹ length u = n ⟹
            tF u ⟹ ftF v ⟹ t ∈ 𝒟 ?lhs› for u v by (fact "*")
    qed

    show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
    proof (elim F_restriction_processptickE)
      assume ‹(t, X) ∈ ℱ (P' △ Q')› ‹length t ≤ n›
      from this(1) consider ‹t ∈ 𝒟 (P' △ Q')›
        | u r where ‹t = u @ [✓(r)]› ‹u @ [✓(r)] ∈ 𝒯 P'›
        | r where ‹✓(r) ∉ X› ‹t @ [✓(r)] ∈ 𝒯 P'›
        | ‹(t, X) ∈ ℱ P'› ‹tF t› ‹([], X) ∈ ℱ Q'›
        | u v where ‹t = u @ v› ‹u ∈ 𝒯 P'› ‹tF u› ‹(v, X) ∈ ℱ Q'› ‹v ≠ []›
        | r where ‹✓(r) ∉ X› ‹t ∈ 𝒯 P'› ‹tF t› ‹[✓(r)] ∈ 𝒯 Q'›
        unfolding Interrupt_projs by blast
      thus ‹(t, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹t ∈ 𝒟 (P' △ Q')›
        hence ‹t ∈ 𝒟 ?rhs› by (simp add: D_restriction_processptickI)
        with div D_F show ‹t ∈ 𝒟 (P' △ Q') ⟹ (t, X) ∈ ℱ ?lhs› by blast
      next
        fix u r assume ‹t = u @ [✓(r)]› ‹u @ [✓(r)] ∈ 𝒯 P'›
        with ‹P ↓ n = P' ↓ n› ‹length t ≤ n› have ‹u @ [✓(r)] ∈ 𝒯 P›
          by (metis T_restriction_processptickI length_le_in_T_restriction_processptick)
        hence ‹(t, X) ∈ ℱ (P △ Q)› by (auto simp add: ‹t = u @ [✓(r)]› F_Interrupt)
        thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_processptickI)
      next
        fix r assume ‹✓(r) ∉ X› ‹t @ [✓(r)] ∈ 𝒯 P'›
        show ‹(t, X) ∈ ℱ ?lhs›
        proof (cases ‹length t = n›)
          assume ‹length t = n›
          with ‹P ↓ n = P' ↓ n› ‹length t ≤ n› ‹t @ [✓(r)] ∈ 𝒯 P'› have ‹t ∈ 𝒯 P›
            by (metis T_restriction_processptickI is_processT3_TR_append
                length_le_in_T_restriction_processptick)
          moreover from ‹t @ [✓(r)] ∈ 𝒯 P'› append_T_imp_tickFree have ‹tF t› by blast
          ultimately have ‹t ∈ 𝒯 (P △ Q)› by (simp add: T_Interrupt)
          with ‹length t = n› ‹tF t› show ‹(t, X) ∈ ℱ ?lhs›
            by (simp add: F_restriction_processptickI)
        next
          assume ‹length t ≠ n›
          with ‹length t ≤ n› have ‹length (t @ [✓(r)]) ≤ n› by simp
          with ‹P ↓ n = P' ↓ n› ‹t @ [✓(r)] ∈ 𝒯 P'› have ‹t @ [✓(r)] ∈ 𝒯 P›
            by (metis T_restriction_processptickI length_le_in_T_restriction_processptick)
          with ‹✓(r) ∉ X› have ‹(t, X) ∈ ℱ (P △ Q)›
            by (simp add: F_Interrupt) (metis Diff_insert_absorb)
          thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_processptickI)
        qed
      next
        assume ‹(t, X) ∈ ℱ P'› ‹tF t› ‹([], X) ∈ ℱ Q'›
        show ‹(t, X) ∈ ℱ ?lhs›
        proof (cases ‹length t = n›)
          assume ‹length t = n›
          from ‹(t, X) ∈ ℱ P'› ‹P ↓ n = P' ↓ n› ‹length t ≤ n› have ‹t ∈ 𝒯 P›
            by (simp add: F_T T_restriction_processptick
                length_le_in_T_restriction_processptick)
          hence ‹t ∈ 𝒯 (P △ Q)› by (simp add: T_Interrupt)
          with ‹length t = n› ‹tF t› show ‹(t, X) ∈ ℱ ?lhs›
            by (simp add: F_restriction_processptickI)
        next
          assume ‹length t ≠ n›
          with ‹length t ≤ n› have ‹length t < n› by simp
          with ‹(t, X) ∈ ℱ P'› ‹P ↓ n = P' ↓ n› ‹length t ≠ n› have ‹(t, X) ∈ ℱ P›
            by (metis F_restriction_processptickI length_less_in_F_restriction_processptick)
          moreover from ‹([], X) ∈ ℱ Q'› have ‹([], X) ∈ ℱ Q›
            by (metis F_restriction_processptickI ‹0 < n› ‹Q ↓ n = Q' ↓ n›
                length_less_in_F_restriction_processptick list.size(3))
          ultimately have ‹(t, X) ∈ ℱ (P △ Q)›
            using ‹tF t› by (simp add: F_Interrupt)
          thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_processptickI)
        qed
      next
        fix u v assume ‹t = u @ v› ‹u ∈ 𝒯 P'› ‹tF u› ‹(v, X) ∈ ℱ Q'› ‹v ≠ []›
        from ‹t = u @ v› ‹length t ≤ n› have ‹length u ≤ n› by simp
        with ‹P ↓ n = P' ↓ n› ‹u ∈ 𝒯 P'› have ‹u ∈ 𝒯 P› 
          by (simp add: T_restriction_processptick length_le_in_T_restriction_processptick)
        show ‹(t, X) ∈ ℱ ?lhs›
        proof (cases ‹length v = n›)
          assume ‹length v = n›
          with ‹t = u @ v› ‹length t ≤ n› have ‹u = []› by simp
          from F_imp_front_tickFree ‹(v, X) ∈ ℱ Q'› have ‹ftF v› by blast
          thus ‹(t, X) ∈ ℱ ?lhs›
          proof (elim front_tickFreeE)
            assume ‹tF v›
            from ‹length v = n› ‹Q ↓ n = Q' ↓ n› ‹(v, X) ∈ ℱ Q'› have ‹v ∈ 𝒯 Q›
              by (metis F_T F_restriction_processptickI dual_order.refl
                  length_le_in_T_restriction_processptick)
            with ‹tF u› ‹u ∈ 𝒯 P› have ‹t ∈ 𝒯 (P △ Q)›
              by (auto simp add: ‹t = u @ v› T_Interrupt)
            with ‹length v = n› ‹t = u @ v› ‹tF v› ‹u = []› show ‹(t, X) ∈ ℱ ?lhs›
              by (simp add: F_restriction_processptickI)
          next
            fix v' r assume ‹v = v' @ [✓(r)]› ‹tF v'›
            with ‹(v, X) ∈ ℱ Q'› ‹length t ≤ n› ‹t = u @ v›
              ‹Q ↓ n = Q' ↓ n› ‹u = []› have ‹v' @ [✓(r)] ∈ 𝒯 Q›
              by (metis F_T T_restriction_processptickI append_self_conv2
                  length_le_in_T_restriction_processptick)
            with ‹t = u @ v› ‹tF u› ‹u ∈ 𝒯 P› ‹v = v' @ [✓(r)]› have ‹t ∈ 𝒯 (P △ Q)›
              by (auto simp add: T_Interrupt)
            thus ‹(t, X) ∈ ℱ ?lhs›
              by (simp add: ‹t = u @ v› ‹u = []› ‹v = v' @ [✓(r)]›
                  restriction_processptick_projs(3) tick_T_F)
          qed
        next
          assume ‹length v ≠ n›
          with ‹length t ≤ n› ‹t = u @ v› have ‹length v < n› by simp
          with ‹Q ↓ n = Q' ↓ n› ‹(v, X) ∈ ℱ Q'› have ‹(v, X) ∈ ℱ Q›
            by (metis F_restriction_processptickI
                length_less_in_F_restriction_processptick)
          with ‹t = u @ v› ‹tF u› ‹u ∈ 𝒯 P› ‹v ≠ []› have ‹(t, X) ∈ ℱ (P △ Q)›
            by (simp add: F_Interrupt) blast
          thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_processptickI)
        qed
      next
        fix r assume ‹✓(r) ∉ X› ‹t ∈ 𝒯 P'› ‹tF t› ‹[✓(r)] ∈ 𝒯 Q'›
        have ‹t ∈ 𝒯 P›
          by (metis T_restriction_processptickI ‹P ↓ n = P' ↓ n› ‹length t ≤ n›
              ‹t ∈ 𝒯 P'› length_le_in_T_restriction_processptick)
        moreover have ‹[✓(r)] ∈ 𝒯 Q›
          by (metis (no_types, lifting) Suc_leI T_restriction_processptick
              Un_iff ‹0 < n› ‹Q ↓ n = Q' ↓ n› ‹[✓(r)] ∈ 𝒯 Q'› length_Cons
              length_le_in_T_restriction_processptick list.size(3))
        ultimately have ‹(t, X) ∈ ℱ (P △ Q)›
          using ‹✓(r) ∉ X› ‹tF t› by (simp add: F_Interrupt) blast
        thus ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_restriction_processptickI)
      qed
    next
      show ‹t = u @ v ⟹ u ∈ 𝒯 (P' △ Q') ⟹ length u = n ⟹
            tF u ⟹ ftF v ⟹ (t, X) ∈ ℱ ?lhs› for u v
        by (simp add: "*" is_processT8)
    qed
  qed
qed


(*<*)
end
  (*>*)