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.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 div : ‹t ∈ 𝒟 (P' ; Q') ⟹ t ∈ 𝒟 (P ; Q ↓ n)› if ‹length t ≤ n› for t
    proof (unfold D_Seq, safe)
      show ‹t ∈ 𝒟 P' ⟹ t ∈ 𝒟 (P ; Q ↓ n)›
        by (simp add: D_restriction_processptick Seq_projs)
          (metis (no_types, opaque_lifting) D_restriction_processptickE
            D_restriction_processptickI ‹P ↓ n = P' ↓ n›)
    next
      fix u r v assume ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 P'› ‹v ∈ 𝒟 Q'›
      from ‹t = u @ v› ‹length t ≤ n› consider ‹v = []› ‹length u = n›
        | ‹u = []› ‹length v = n› | ‹length u < n› ‹length v < n›
        using nless_le by (cases u; cases v, auto)
      thus ‹u @ v ∈ 𝒟 (P ; Q ↓ n)›
      proof cases
        assume ‹v = []› ‹length u = n›
        from ‹u @ [✓(r)] ∈ 𝒯 P'› append_T_imp_tickFree is_processT3_TR_append
        have ‹tF u› ‹u ∈ 𝒯 P'› by auto
        from ‹u ∈ 𝒯 P'› ‹length u = n› ‹P ↓ n = P' ↓ n› have ‹u ∈ 𝒯 P›
          by (metis T_restriction_processptickI less_or_eq_imp_le
              length_le_in_T_restriction_processptick)
        with ‹tF u› have ‹u ∈ 𝒯 (P ; Q)› by (simp add: T_Seq)
        with ‹length u = n› show ‹u @ v ∈ 𝒟 (P ; Q ↓ n)›
          by (simp add: ‹v = []› ‹tF u› D_restriction_processptickI)
      next
        assume ‹u = []› ‹length v = n›
        from ‹0 < n› ‹u @ [✓(r)] ∈ 𝒯 P'› ‹u = []› ‹P ↓ n = P' ↓ n›
        have ‹[✓(r)] ∈ 𝒯 P›
          by (cases n, simp_all)
            (metis Suc_leI T_restriction_processptickI length_Cons
              length_le_in_T_restriction_processptick list.size(3) zero_less_Suc)
        show ‹u @ v ∈ 𝒟 (P ; Q ↓ n)›
        proof (cases ‹tF v›)
          assume ‹tF v›
          have ‹v ∈ 𝒯 Q'› by (simp add: D_T ‹v ∈ 𝒟 Q'›)
          with ‹length v = n› ‹Q ↓ n = Q' ↓ n› have ‹v ∈ 𝒯 Q›
            unfolding restriction_fun_def
            by (metis T_restriction_processptickI less_or_eq_imp_le
                length_le_in_T_restriction_processptick)
          with ‹[✓(r)] ∈ 𝒯 P› have ‹v ∈ 𝒯 (P ; Q)›
            by (simp add: T_Seq) (metis append_Nil)
          with ‹length v = n› show ‹u @ v ∈ 𝒟 (P ; Q ↓ n)›
            by (simp add: ‹u = []› ‹tF v› D_restriction_processptickI)
        next
          assume ‹¬ tF v›
          with ‹u = []› ‹Q ↓ n = Q' ↓ n› ‹¬ tF v› ‹length t ≤ n›
            ‹t = u @ v› ‹v ∈ 𝒟 Q'› have ‹v ∈ 𝒟 Q›
            by (metis append_self_conv2 not_tickFree_in_D_restriction_processptick_iff)
          with ‹[✓(r)] ∈ 𝒯 P› have ‹v ∈ 𝒟 (P ; Q)›
            by (simp add: D_Seq) (metis append_Nil)
          thus ‹u @ v ∈ 𝒟 (P ; Q ↓ n)›
            by (simp add: D_restriction_processptickI ‹u = []›)
        qed
      next
        assume ‹length u < n› ‹length v < n›
        from ‹u @ [✓(r)] ∈ 𝒯 P'› ‹length u < n› ‹P ↓ n = P' ↓ n›
        have ‹u @ [✓(r)] ∈ 𝒯 P›
          by (metis length_le_in_T_restriction_processptick Suc_le_eq 
              length_append_singleton T_restriction_processptickI)
        moreover from ‹v ∈ 𝒟 Q'› ‹length v < n› ‹Q ↓ n = Q' ↓ n›
        have ‹v ∈ 𝒟 Q›
          by (metis D_restriction_processptickI length_less_in_D_restriction_processptick)
        ultimately show ‹u @ v ∈ 𝒟 (P ; Q ↓ n)›
          by (auto simp add: D_restriction_processptick D_Seq)
      qed
    qed

    fix t X assume ‹(t, X) ∈ ℱ (P' ; Q')› ‹length t ≤ n›
    consider ‹t ∈ 𝒟 (P' ; Q')› | ‹(t, X ∪ range tick) ∈ ℱ P'› ‹tF t›
      | u r v where ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 P'› ‹(v, X) ∈ ℱ Q'›
      using ‹(t, X) ∈ ℱ (P' ; Q')› by (auto simp add: Seq_projs)
    thus ‹(t, X) ∈ ℱ (P ; Q ↓ n)›
    proof cases
      from div ‹length t ≤ n› D_F
      show ‹t ∈ 𝒟 (P' ; Q') ⟹ (t, X) ∈ ℱ (P ; Q ↓ n)› by blast
    next
      show ‹(t, X) ∈ ℱ (P ; Q ↓ n)› if ‹(t, X ∪ range tick) ∈ ℱ P'› ‹tF t›
      proof (cases ‹length t = n›)
        assume ‹length t = n›
        from ‹(t, X ∪ range tick) ∈ ℱ P'› have ‹t ∈ 𝒯 P'› by (simp add: F_T)
        with ‹P ↓ n = P' ↓ n› ‹length t ≤ n› have ‹t ∈ 𝒯 P›
          by (metis T_restriction_processptickI length_le_in_T_restriction_processptick)
        with ‹tF t› have ‹t ∈ 𝒯 (P ; Q)› by (simp add: T_Seq)
        with ‹length t = n› ‹tF t› show ‹(t, X) ∈ ℱ (P ; Q ↓ n)›
          by (simp add: F_restriction_processptickI)
      next
        assume ‹length t ≠ n›
        with ‹length t ≤ n› have ‹length t < n› by linarith
        with ‹P ↓ n = P' ↓ n› ‹(t, X ∪ range tick) ∈ ℱ P'›
        have ‹(t, X ∪ range tick) ∈ ℱ P›
          by (metis F_restriction_processptickI length_less_in_F_restriction_processptick)
        with ‹tF t› show ‹(t, X) ∈ ℱ (P ; Q ↓ n)›
          by (simp add: F_restriction_processptickI F_Seq)
      qed
    next
      fix u r v assume ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 P'› ‹(v, X) ∈ ℱ Q'›
      from ‹t = u @ v› ‹length t ≤ n› consider ‹v = []› ‹length u = n›
        | ‹u = []› ‹length v = n› | ‹length u < n› ‹length v < n›
        using nless_le by (cases u; cases v, auto)
      thus ‹(t, X) ∈ ℱ (P ; Q ↓ n)›
      proof cases
        assume ‹v = []› ‹length u = n›
        from ‹u @ [✓(r)] ∈ 𝒯 P'› append_T_imp_tickFree is_processT3_TR_append
        have ‹tF u› ‹u ∈ 𝒯 P'› by auto
        from ‹u ∈ 𝒯 P'› ‹length u = n› ‹P ↓ n = P' ↓ n› have ‹u ∈ 𝒯 P›
          by (metis T_restriction_processptickI less_or_eq_imp_le
              length_le_in_T_restriction_processptick)
        with ‹tF u› have ‹u ∈ 𝒯 (P ; Q)› by (simp add: T_Seq)
        with ‹length u = n› show ‹(t, X) ∈ ℱ (P ; Q ↓ n)›
          by (simp add: ‹v = []› ‹tF u› F_restriction_processptick)
            (use ‹t = u @ v› ‹tF u› ‹v = []› front_tickFree_Nil in blast)
      next
        assume ‹u = []› ‹length v = n›
        from ‹0 < n› ‹u @ [✓(r)] ∈ 𝒯 P'› ‹u = []› ‹P ↓ n = P' ↓ n›
        have ‹[✓(r)] ∈ 𝒯 P›
          by (cases n, simp_all)
            (metis Suc_leI T_restriction_processptickI length_Cons
              length_le_in_T_restriction_processptick list.size(3) zero_less_Suc)
        show ‹(t, X) ∈ ℱ (P ; Q ↓ n)›
        proof (cases ‹tF v›)
          assume ‹tF v›
          from F_T ‹(v, X) ∈ ℱ Q'› have ‹v ∈ 𝒯 Q'› by blast
          with ‹length v = n› ‹Q ↓ n = Q' ↓ n› have ‹v ∈ 𝒯 Q›
            unfolding restriction_fun_def
            by (metis T_restriction_processptickI less_or_eq_imp_le
                length_le_in_T_restriction_processptick)
          with ‹[✓(r)] ∈ 𝒯 P› have ‹v ∈ 𝒯 (P ; Q)›
            by (simp add: T_Seq) (metis append_Nil)
          with ‹length v = n› have ‹t ∈ 𝒟 (P ; Q ↓ n)›
            by (simp add: ‹u = []› ‹tF v› ‹t = u @ v› D_restriction_processptickI)
          with D_F show ‹(t, X) ∈ ℱ (P ; Q ↓ n)› by blast
        next
          assume ‹¬ tF v›
          with ‹u = []› ‹Q ↓ n = Q' ↓ n› ‹¬ tF v› ‹length t ≤ n›
            ‹t = u @ v› ‹(v, X) ∈ ℱ Q'› have ‹(v, X) ∈ ℱ Q›
            by (metis append_self_conv2 not_tickFree_in_F_restriction_processptick_iff)
          with ‹[✓(r)] ∈ 𝒯 P› have ‹(t, X) ∈ ℱ (P ; Q)›
            by (simp add: ‹t = u @ v› ‹u = []› F_Seq) (metis append_Nil)
          thus ‹(t, X) ∈ ℱ (P ; Q ↓ n)›
            by (simp add: F_restriction_processptickI)
        qed
      next
        assume ‹length u < n› ‹length v < n›
        from ‹u @ [✓(r)] ∈ 𝒯 P'› ‹length u < n› ‹P ↓ n = P' ↓ n›
        have ‹u @ [✓(r)] ∈ 𝒯 P›
          by (metis length_le_in_T_restriction_processptick Suc_le_eq 
              length_append_singleton T_restriction_processptickI)
        moreover from ‹(v, X) ∈ ℱ Q'› ‹length v < n› ‹Q ↓ n = Q' ↓ n›
        have ‹(v, X) ∈ ℱ Q›
          by (metis F_restriction_processptickI length_less_in_F_restriction_processptick)
        ultimately show ‹(t, X) ∈ ℱ (P ; Q ↓ n)›
          by (auto simp add: ‹t = u @ v› F_restriction_processptick F_Seq)
      qed
    qed
  qed
qed



(*<*)
end
  (*>*)