Theory Sequential_Composition_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 Sequential Composition›

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

subsection ‹Refinement›

lemma restriction_processptick_Seq_FD :
  ‹P ; Q ↓ n ⊑FD (P ↓ n) ; (Q ↓ n)› (is ‹?lhs ⊑FD ?rhs›)
proof -
  have * : ‹t ∈ 𝒟 (P ↓ n) ⟹ t ∈ 𝒟 ?lhs› for t
    by (elim D_restriction_processptickE)
      (auto simp add: Seq_projs D_restriction_processptick)
  { fix t u v r w x
    assume ‹u @ [✓(r)] ∈ 𝒯 P› ‹length u < n› ‹v = w @ x› ‹w ∈ 𝒯 Q›
      ‹length w = n› ‹tF w› ‹ftF x› ‹t = u @ v›
    hence ‹t = (u @ take (n - length u) w) @ drop (n - length u) w @ x ∧
           u @ take (n - length u) w ∈ 𝒯 (P ; Q) ∧
           length (u @ take (n - length u) w) = n ∧
           tF (u @ take (n - length u) w) ∧ ftF (drop (n - length u) w @ x)›
      by (simp add: ‹t = u @ v› T_Seq)
        (metis append_T_imp_tickFree append_take_drop_id front_tickFree_append
          is_processT3_TR_append list.distinct(1) tickFree_append_iff)
    with D_restriction_processptick have ‹t ∈ 𝒟 ?lhs› by blast
  } note ** = this

  show ‹?lhs ⊑FD ?rhs›
  proof (unfold refine_defs, safe)
    show div : ‹t ∈ 𝒟 ?lhs› if ‹t ∈ 𝒟 ?rhs› for t
    proof -
      from ‹t ∈ 𝒟 ?rhs› consider ‹t ∈ 𝒟 (P ↓ n)›
        | u v r where ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 (P ↓ n)› ‹v ∈ 𝒟 (Q ↓ n)›
        unfolding D_Seq by blast
      thus ‹t ∈ 𝒟 ?lhs›
      proof cases
        show ‹t ∈ 𝒟 (P ↓ n) ⟹ t ∈ 𝒟 ?lhs› by (fact "*")
      next
        fix u v r assume ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 (P ↓ n)› ‹v ∈ 𝒟 (Q ↓ n)›
        from ‹u @ [✓(r)] ∈ 𝒯 (P ↓ n)› consider ‹u @ [✓(r)] ∈ 𝒟 (P ↓ n)› | ‹u @ [✓(r)] ∈ 𝒯 P› ‹length u < n›
          by (elim T_restriction_processptickE) (auto simp add: D_restriction_processptick)
        thus ‹t ∈ 𝒟 ?lhs›
        proof cases
          show ‹u @ [✓(r)] ∈ 𝒟 (P ↓ n) ⟹ t ∈ 𝒟 ?lhs›
            by (metis "*" D_imp_front_tickFree ‹t = u @ v› ‹v ∈ 𝒟 (Q ↓ n)›
                front_tickFree_append_iff is_processT7 is_processT9 not_Cons_self)
        next
          from ‹v ∈ 𝒟 (Q ↓ n)› show ‹u @ [✓(r)] ∈ 𝒯 P ⟹ length u < n ⟹ t ∈ 𝒟 ?lhs›
          proof (elim D_restriction_processptickE exE conjE)
            show ‹u @ [✓(r)] ∈ 𝒯 P ⟹ v ∈ 𝒟 Q ⟹ t ∈ 𝒟 ?lhs›
              by (simp add: ‹t = u @ v› D_restriction_processptick D_Seq) blast
          next
            show ‹⟦u @ [✓(r)] ∈ 𝒯 P; length u < n; v = w @ x; w ∈ 𝒯 Q;
                   length w = n; tF w; ftF x⟧ ⟹ t ∈ 𝒟 ?lhs› for w x
              using "**" ‹t = u @ v› by blast
          qed
        qed
      qed
    qed

    have mono : ‹(P ↓ n) ; (Q ↓ n) ⊑ P ; Q›
      by (simp add: fun_below_iff mono_Seq restriction_fun_def
          restriction_processptick_approx_self)

    show ‹(t, X) ∈ ℱ ?lhs› if ‹(t, X) ∈ ℱ ?rhs› for t X
      by (meson F_restriction_processptickI div is_processT8 mono proc_ord2a that)
  qed
qed


corollary restriction_processptick_MultiSeq_FD :
  ‹(SEQ l ∈@ L. P l) ↓ n ⊑FD SEQ l ∈@ L. (P l ↓ n)›
proof (induct L rule: rev_induct)
  show ‹(SEQ l ∈@ []. P l) ↓ n ⊑FD SEQ l ∈@ []. (P l ↓ n)› by simp
next
  fix a L
  assume hyp: ‹(SEQ l ∈@ L. P l) ↓ n ⊑FD SEQ l ∈@ L. (P l ↓ n)›
  have ‹(SEQ l ∈@ (L @ [a]). P l) ↓ n = (SEQ l ∈@ L. P l ; P a) ↓ n› by simp
  also have ‹… ⊑FD SEQ l ∈@ L. (P l ↓ n) ; (P a ↓ n)›
    by (fact trans_FD[OF restriction_processptick_Seq_FD mono_Seq_FD[OF hyp idem_FD]])
  also have ‹… = SEQ l∈@(L @ [a]). (P l ↓ n)› by simp
  finally show ‹(SEQ l ∈@ (L @ [a]). P l) ↓ n ⊑FD …› .
qed



subsection ‹Non Destructiveness›

lemma Seq_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)
  show ‹P ; Q ↓ n ⊑FD P' ; Q' ↓ n›
  proof (rule leFD_restriction_processptickI)
    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_Seq_FD restriction_processptick_FD_self
                restriction_processptick_Seq_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_Seq_FD
                restriction_processptick_FD_self
                restriction_processptick_Seq_FD subset_iff)
  qed
qed



(*<*)
end
  (*>*)