Theory Sequential_Composition_Generalized_Non_Destructive

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, 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
 ***********************************************************************************)


chapter ‹Non Destructiveness Rules›

(*<*)
theory Sequential_Composition_Generalized_Non_Destructive
  imports "HOL-CSP_RS" CSP_PTick_Monotonicities
begin
  (*<*)


section ‹Sequential Composition›

subsection ‹Refinement›

lemma restriction_processptick_Seqptick_FD :
  ‹P ;✓ Q ↓ n ⊑FD (P ↓ n) ;✓ (Q ↓ n)› (is ‹?lhs ⊑FD ?rhs›)
proof -
  show ‹?lhs ⊑FD ?rhs›
  proof (rule failure_divergence_refine_optimizedI)
    { fix t assume ‹tF t› and ‹t ∈ 𝒟 ?rhs›
      from this(2) consider (D_P) u v where ‹t = map (ev ∘ of_ev) u @ v› ‹u ∈ 𝒟 (P ↓ n)› ‹tF u› ‹ftF v›
        | (D_Q) u r v where ‹t = map (ev ∘ of_ev) u @ v› ‹u @ [✓(r)] ∈ 𝒯 P› ‹length u < n› ‹tF u› ‹v ∈ 𝒟 ((Q ↓ n) r)›
        by (auto simp add: Seqptick_projs restriction_processptick_projs)
         (metis D_P D_imp_front_tickFree D_restriction_processptickI is_processT3_TR_append linorder_less_linear,
           metis D_P D_imp_front_tickFree D_restriction_processptickI is_processT7 is_processT9)
      hence ‹t ∈ 𝒟 ?lhs›
      proof cases
        case D_P thus ‹t ∈ 𝒟 ?lhs›
          by (elim D_restriction_processptickE, simp_all add: Seqptick_projs D_restriction_processptick)
            (metis, metis front_tickFree_append length_map tickFree_map_ev_comp)
      next
        case D_Q
        from D_Q(5) show ‹t ∈ 𝒟 ?lhs›
        proof (unfold restriction_fun_def, elim D_restriction_processptickE)
          assume ‹v ∈ 𝒟 (Q r)›
          with D_Q(1, 2, 4) have ‹t ∈ 𝒟 (P ;✓ Q)› by (auto simp add: Seqptick_projs)
          thus ‹t ∈ 𝒟 ?lhs› by (simp add: D_restriction_processptickI)
        next
          fix w x assume ‹v = w @ x› ‹w ∈ 𝒯 (Q r)› ‹length w = n› ‹tF w› ‹ftF x›
          from D_Q(2, 4) ‹w ∈ 𝒯 (Q r)› have ‹map (ev ∘ of_ev) u @ w ∈ 𝒯 (P ;✓ Q)›
            by (auto simp add: Seqptick_projs)
          moreover have ‹tF (map (ev ∘ of_ev) u @ w)› by (simp add: ‹tF w›)
          moreover have ‹n ≤ length (map (ev ∘ of_ev) u @ w)›
            by (simp add: ‹length w = n›)
          ultimately have ‹map (ev ∘ of_ev) u @ w ∈ 𝒟 ?lhs›
            by (metis D_restriction_processptickI antisym_conv2)
          with D_Q(1) ‹tF t› ‹v = w @ x› is_processT7 show ‹t ∈ 𝒟 (P ;✓ Q ↓ n)› by fastforce
        qed
      qed
    }
    thus ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
      by (metis D_imp_front_tickFree div_butlast_when_non_tickFree_iff front_tickFree_iff_tickFree_butlast)
  next
    have ‹(P ↓ n) ;✓ (Q ↓ n) ⊑ P ;✓ Q›
      by (simp add: fun_below_iff mono_Seqptick restriction_fun_def
          restriction_processptick_approx_self)
    thus ‹(t, X) ∈ ℱ ?rhs ⟹ 𝒟 ((P ↓ n) ;✓ (Q ↓ n)) ⊆ 𝒟 (P ;✓ Q ↓ n) ⟹
          (t, X) ∈ ℱ ?lhs› for t X
      by (meson F_restriction_processptickI in_mono is_processT8 le_approx2)
  qed
qed


corollary restriction_processptick_MultiSeqptick_FD :
  ‹((SEQ✓ l ∈@ L. P l) ↓ n) r ⊑FD (SEQ✓ l ∈@ L. (P l ↓ n)) r›
proof (induct L arbitrary: r)
  show ‹((SEQ✓ l ∈@ []. P l) ↓ n) r ⊑FD (SEQ✓ l ∈@ []. (P l ↓ n)) r› for r
    by (simp add: restriction_fun_def)
next
  fix a L r
  assume hyp: ‹((SEQ✓ l ∈@ L. P l) ↓ n) r ⊑FD (SEQ✓ l ∈@ L. (P l ↓ n)) r› for r
  have ‹((SEQ✓ l ∈@ (a # L). P l) ↓ n) r = P a r ;✓ (SEQ✓ l ∈@ L. P l) ↓ n›
    by (simp add: restriction_fun_def)
  also have ‹… ⊑FD (P a r ↓ n) ;✓ SEQ✓ l ∈@ L. (P l ↓ n)›
    by (fact trans_FD[OF restriction_processptick_Seqptick_FD mono_Seqptick_FD[OF idem_FD hyp]])
  also have ‹… = (SEQ✓ l ∈@ (a # L). (P l ↓ n)) r›
    by (simp add: restriction_fun_def)
  finally show ‹((SEQ✓ l ∈@ (a # L). P l) ↓ n) r ⊑FD …› .
qed


subsection ‹Non Destructiveness›

lemma Seqptick_non_destructive :
  ‹non_destructive (λ(P, Q :: 'r ⇒ ('a, 's) processptick). P ;✓ Q)›
proof (rule order_non_destructiveI, clarify)
  fix P P' :: ‹('a, 'r) processptick› and Q Q' :: ‹'r ⇒ ('a, 's) 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_Seqptick_FD restriction_fun_def restriction_processptick_FD_self
                restriction_processptick_Seqptick_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_Seqptick_FD
                restriction_fun_def restriction_processptick_FD_self
                restriction_processptick_Seqptick_FD subset_iff)
  qed
qed



subsection ‹Setup›

text ‹
We also introduce a third law: the assumption of constructiveness for term‹g› can be
weakened to non destructiveness if we cannot directly perform a tick on the left.
›

lemma Seqptick_restriction_shift_processptick :
  ‹non_destructive f ⟹ non_destructive g ⟹ non_destructive (λx. f x ;✓ g x)›
  ‹constructive f ⟹ constructive g ⟹ constructive (λx. f x ;✓ g x)›
  ‹constructive f ⟹ non_destructive g ⟹ (⋀x r. ✓(r) ∉ (f x)0) ⟹ constructive (λx. f x ;✓ g x)›
  for f :: ‹'b :: restriction ⇒ ('a, 'r) processptick›
  ― ‹TODO: this can probably by strengthened with a notion of strict initials›
proof -
  show ‹non_destructive f ⟹ non_destructive g ⟹ non_destructive (λx. f x ;✓ g x)›
    by (fact non_destructive_comp_non_destructive
        [OF Seqptick_non_destructive non_destructive_prod_codomain, simplified])
next
  show ‹constructive f ⟹ constructive g ⟹ constructive (λx. f x ;✓ g x)›
    by (fact non_destructive_comp_constructive
        [OF Seqptick_non_destructive constructive_prod_codomain, simplified])
next
  show ‹constructive (λx. f x ;✓ g x)›
    if ‹constructive f› and ‹non_destructive g› and ‹⋀x r. ✓(r) ∉ (f x)0›
  proof (rule order_constructiveI)
    fix x y :: 'b and n assume ‹x ↓ n = y ↓ n›
    with that(1, 2) have ‹f x ↓ Suc n = f y ↓ Suc n› and ‹g x ↓ n = g y ↓ n›
      by (auto dest: non_destructiveD constructiveD)
    show ‹f x ;✓ g x ↓ Suc n ⊑FD f y ;✓ g y ↓ Suc n›
    proof (rule leFD_restriction_processptickI)
      show div : ‹t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)› if ‹length t ≤ Suc n› and ‹t ∈ 𝒟 (f y ;✓ g y)› for t
      proof (cases n)
        assume ‹n = 0›
        with ‹length t ≤ Suc n› ‹t ∈ 𝒟 (f y ;✓ g y)› ‹f x ↓ Suc n = f y ↓ Suc n› ‹⋀r. ✓(r) ∉ (f y)0›
        show ‹t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
          by (auto simp add: D_restriction_processptick Seqptick_projs)
            (metis D_T D_restriction_processptickI add_leE length_le_in_T_restriction_processptick
                   length_less_in_D_restriction_processptick length_map order_le_imp_less_or_eq tickFree_map_ev_comp,
              metis T_restriction_processptickI add_leD1 front_tickFree_Nil initials_memI' is_processT3_TR_append
                    le_SucE length_greater_0_conv length_le_in_T_restriction_processptick length_map
                    less_numeral_extra(3) one_is_add order_less_le_trans self_append_conv2 tickFree_map_ev_comp)
      next
        fix k assume ‹n = Suc k›
        from ‹t ∈ 𝒟 (f y ;✓ g y)›
        consider (D_P) u v where ‹t = map (ev ∘ of_ev) u @ v› ‹u ∈ 𝒟 (f y)› ‹tF u› ‹ftF v›
          | (D_Q) u r v where ‹t = map (ev ∘ of_ev) u @ v› ‹u @ [✓(r)] ∈ 𝒯 (f y)› ‹tF u› ‹v ∈ 𝒟 (g y r)›
          unfolding Seqptick_projs by blast
        thus ‹t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
        proof cases
          case D_P
          with  ‹f x ↓ Suc n = f y ↓ Suc n› show ‹t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
            by (simp add: D_restriction_processptick Seqptick_projs)
              (metis D_T D_restriction_processptickI length_append length_le_in_T_restriction_processptick
                     length_less_in_D_restriction_processptick length_map linorder_not_less
                     not_less_iff_gr_or_eq that(1) tickFree_map_ev_comp trans_less_add1)
        next
          case D_Q
          from ‹✓(r) ∉ (f y)0› D_Q(2, 3) obtain a u' where ‹u = ev a # u'›
            by (metis append_Nil eventptick.collapse(1) initials_memI neq_Nil_conv tickFree_Cons_iff)
          with ‹length t ≤ Suc n› D_Q(1)
          consider ‹v = []› ‹length u = Suc n› | ‹u' = []› ‹length v = n› | ‹length u ≤ n› ‹length v < n›
            by simp
              (metis (no_types, opaque_lifting) add_cancel_right_right add_leD2 add_le_same_cancel2
                     antisym length_greater_0_conv linorder_not_less not_less_eq_eq trans_le_add1)
          thus ‹t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
          proof cases
            from D_Q(1-3) ‹f x ↓ Suc n = f y ↓ Suc n›
            show ‹v = [] ⟹ length u = Suc n ⟹ t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
              by (simp add: D_restriction_processptick Seqptick_projs)
                (metis T_restriction_processptickI front_tickFree_Nil is_processT3_TR_append le_Suc_eq
                       length_le_in_T_restriction_processptick length_map self_append_conv tickFree_map_ev_comp)
          next
            assume ‹u' = []› ‹length v = n›
            from ‹f x ↓ Suc n = f y ↓ Suc n› ‹n = Suc k› ‹u = ev a # u'› ‹u' = []›
            have ‹u @ [✓(r)] ∈ 𝒯 (f x)›
              by simp
                (smt (verit, best) D_Q(2) D_T One_nat_def T_F_spec add_Suc_shift append_Cons
                     append_self_conv2 le_add1 le_approx2 length_Cons list.size(3)
                     non_tickFree_tick not_tickFree_in_D_restriction_processptick_iff plus_1_eq_Suc
                     restriction_processptick_approx_self tickFree_append_iff)
            from D_Q(4) consider ‹tF v› ‹v ∈ 𝒯 (g x r)› | ‹¬ tF v› ‹v ∈ 𝒟 (g x r)›
              by (metis D_T D_restriction_processptickI ‹g x ↓ n = g y ↓ n› ‹length v = n› dual_order.refl
                  length_le_in_T_restriction_processptick not_tickFree_in_D_restriction_processptick_iff restriction_fun_def)
            thus ‹t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
            proof cases
              assume ‹tF v› ‹v ∈ 𝒯 (g x r)›
              from D_Q(3) ‹u @ [✓(r)] ∈ 𝒯 (f x)› ‹v ∈ 𝒯 (g x r)›
              have ‹map (ev ∘ of_ev) u @ v ∈ 𝒯 (f x ;✓ g x)›
                by (auto simp add: Seqptick_projs)
              moreover have ‹tF (map (ev ∘ of_ev) u @ v)› by (simp add: ‹tF v›)
              moreover have ‹length (map (ev ∘ of_ev) u @ v) = Suc n›
                by (simp add: ‹length v = n› ‹u = ev a # u'› ‹u' = []›)
              ultimately show ‹t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
                by (metis D_Q(1) D_restriction_processptickI)
            next
              from ‹u @ [✓(r)] ∈ 𝒯 (f x)› D_Q(1, 3)
              show ‹¬ tF v ⟹ v ∈ 𝒟 (g x r) ⟹ t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
                by (auto simp add: D_restriction_processptick Seqptick_projs)
            qed
          next
            assume ‹length u ≤ n› ‹length v < n›
            have ‹u @ [✓(r)] ∈ 𝒯 (f x)›
              by (metis D_Q(2) T_restriction_processptickI ‹f x ↓ Suc n = f y ↓ Suc n› ‹length u ≤ n› length_append_singleton
                  length_le_in_T_restriction_processptick nat_add_left_cancel_le plus_1_eq_Suc)
            moreover have ‹v ∈ 𝒟 (g x r)›
              by (metis D_Q(4) D_restriction_processptickI ‹g x ↓ n = g y ↓ n› ‹length v < n›
                        length_less_in_D_restriction_processptick restriction_fun_def)
            ultimately have ‹map (ev ∘ of_ev) u @ v ∈ 𝒟 (f x ;✓ g x)›
              by (simp add: Seqptick_projs) (use D_Q(3) in blast)
            thus ‹t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
              by (simp add: D_Q(1) D_restriction_processptickI)
          qed
        qed
      qed

      fix t X assume ‹length t ≤ Suc n› ‹(t, X) ∈ ℱ (f y ;✓ g y)›
      show ‹(t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)›
      proof (cases n)
        assume ‹n = 0›
        with ‹length t ≤ Suc n› ‹(t, X) ∈ ℱ (f y ;✓ g y)› ‹f x ↓ Suc n = f y ↓ Suc n› ‹⋀r. ✓(r) ∉ (f y)0›
        show ‹(t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)›
          by (auto simp add: F_restriction_processptick Seqptick_projs)
            (metis F_T F_restriction_processptickI antisym_conv2 append_Nil2 front_tickFree_Nil
                   length_le_in_T_restriction_processptick length_less_in_F_restriction_processptick
                   length_map tickFree_map_ev_comp,
              metis add_leE front_tickFree_Nil initials_memI is_processT3_TR_append le_Suc_eq le_ref2T
                    le_zero_eq length_0_conv length_le_in_T_restriction_processptick length_map one_is_add
                    restriction_processptick_FD_self self_append_conv2 subset_iff tickFree_map_ev_comp,
              metis D_T D_restriction_processptickI add_leD1 le_SucE le_imp_less_Suc
                    length_le_in_T_restriction_processptick length_less_in_D_restriction_processptick
                    length_map tickFree_map_ev_comp)
      next
        fix k assume ‹n = Suc k›
        from ‹(t, X) ∈ ℱ (f y ;✓ g y)› consider ‹t ∈ 𝒟 (f y ;✓ g y)›
        | (F_P) u where ‹t = map (ev ∘ of_ev) u› ‹(u, ref_Seqptick X) ∈ ℱ (f y)› ‹tF u›
        | (F_Q) u r v where ‹t = map (ev ∘ of_ev) u @ v› ‹u @ [✓(r)] ∈ 𝒯 (f y)› ‹tF u› ‹(v, X) ∈ ℱ (g y r)›
        unfolding Seqptick_projs by fast
      thus ‹(t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)›
      proof cases
        from div ‹length t ≤ Suc n› is_processT8
        show ‹t ∈ 𝒟 (f y ;✓ g y) ⟹ (t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)› by blast
      next
        case F_P
        from ‹length t ≤ Suc n› consider ‹length u ≤ n› | ‹length u = Suc n›
          by (simp add: F_P(1)) linarith
        thus ‹(t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)›
        proof cases
          assume ‹length u ≤ n›
          with ‹f x ↓ Suc n = f y ↓ Suc n› F_P(2)
          have ‹(u, ref_Seqptick X) ∈ ℱ (f x)›
            by (metis F_restriction_processptickI less_Suc_eq_le
                length_less_in_F_restriction_processptick)
          with F_P(1, 3) have ‹(t, X) ∈ ℱ (f x ;✓ g x)› by (auto simp add: Seqptick_projs)
          thus ‹(t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)›
            by (simp add: F_restriction_processptickI)
        next
          assume ‹length u = Suc n›
          with F_P ‹f x ↓ Suc n = f y ↓ Suc n›
          have ‹t ∈ 𝒯 (f x ;✓ g x)›
            by (simp add: Seqptick_projs)
              (metis F_T T_restriction_processptickI le_Suc_eq length_le_in_T_restriction_processptick)
          moreover have ‹length t = Suc n› by (simp add: F_P(1) ‹length u = Suc n›)
          moreover have ‹tF t› by (simp add: F_P(1))
          ultimately have ‹t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
            by (simp add: D_restriction_processptickI)
          thus ‹(t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)› by (fact is_processT8)
        qed
      next
        case F_Q
        from ‹✓(r) ∉ (f y)0› F_Q(2, 3) obtain a u' where ‹u = ev a # u'›
            by (metis append_Nil eventptick.collapse(1) initials_memI neq_Nil_conv tickFree_Cons_iff)
          with ‹length t ≤ Suc n› F_Q(1)
          consider ‹v = []› ‹length u = Suc n› | ‹u' = []› ‹length v = n› | ‹length u ≤ n› ‹length v < n›
            by simp
              (metis (no_types, opaque_lifting) add_cancel_right_right add_leD2 add_le_same_cancel2
                     antisym length_greater_0_conv linorder_not_less not_less_eq_eq trans_le_add1)
          thus ‹(t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)›
          proof cases
            from F_Q(1-3) ‹f x ↓ Suc n = f y ↓ Suc n›
            show ‹v = [] ⟹ length u = Suc n ⟹ (t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)›
              by (simp add: F_restriction_processptick Seqptick_projs)
                (metis T_restriction_processptickI front_tickFree_Nil is_processT3_TR_append le_Suc_eq
                       length_le_in_T_restriction_processptick length_map self_append_conv tickFree_map_ev_comp)
          next
            assume ‹u' = []› ‹length v = n›
            from ‹f x ↓ Suc n = f y ↓ Suc n› ‹n = Suc k› ‹u = ev a # u'› ‹u' = []›
            have ‹u @ [✓(r)] ∈ 𝒯 (f x)›
              by simp
                (smt (verit, best) F_Q(2) D_T One_nat_def T_F_spec add_Suc_shift append_Cons
                     append_self_conv2 le_add1 le_approx2 length_Cons list.size(3)
                     non_tickFree_tick not_tickFree_in_D_restriction_processptick_iff plus_1_eq_Suc
                     restriction_processptick_approx_self tickFree_append_iff)
            from F_Q(4) consider ‹tF v› ‹v ∈ 𝒯 (g x r)› | ‹¬ tF v› ‹(v, X) ∈ ℱ (g x r)›
              by (metis F_T F_restriction_processptickI ‹g x ↓ n = g y ↓ n› ‹length v = n› dual_order.refl
                  length_le_in_T_restriction_processptick not_tickFree_in_F_restriction_processptick_iff restriction_fun_def)
            thus ‹(t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)›
            proof cases
              assume ‹tF v› ‹v ∈ 𝒯 (g x r)›
              from F_Q(3) ‹u @ [✓(r)] ∈ 𝒯 (f x)› ‹v ∈ 𝒯 (g x r)›
              have ‹map (ev ∘ of_ev) u @ v ∈ 𝒯 (f x ;✓ g x)›
                by (auto simp add: Seqptick_projs)
              moreover have ‹tF (map (ev ∘ of_ev) u @ v)› by (simp add: ‹tF v›)
              moreover have ‹length (map (ev ∘ of_ev) u @ v) = Suc n›
                by (simp add: ‹length v = n› ‹u = ev a # u'› ‹u' = []›)
              ultimately have ‹t ∈ 𝒟 (f x ;✓ g x ↓ Suc n)›
                by (metis F_Q(1) D_restriction_processptickI)
              thus ‹(t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)› by (fact is_processT8)
            next
              from ‹u @ [✓(r)] ∈ 𝒯 (f x)› F_Q(1, 3)
              show ‹¬ tF v ⟹ (v, X) ∈ ℱ (g x r) ⟹ (t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)›
                by (auto simp add: F_restriction_processptick Seqptick_projs)
            qed
          next
            assume ‹length u ≤ n› ‹length v < n›
            have ‹u @ [✓(r)] ∈ 𝒯 (f x)›
              by (metis F_Q(2) T_restriction_processptickI ‹f x ↓ Suc n = f y ↓ Suc n› ‹length u ≤ n› length_append_singleton
                  length_le_in_T_restriction_processptick nat_add_left_cancel_le plus_1_eq_Suc)
            moreover have ‹(v, X) ∈ ℱ (g x r)›
              by (metis F_Q(4) F_restriction_processptickI ‹g x ↓ n = g y ↓ n› ‹length v < n›
                        length_less_in_F_restriction_processptick restriction_fun_def)
            ultimately have ‹(map (ev ∘ of_ev) u @ v, X) ∈ ℱ (f x ;✓ g x)›
              by (simp add: Seqptick_projs) (use F_Q(3) in blast)
            thus ‹(t, X) ∈ ℱ (f x ;✓ g x ↓ Suc n)›
              by (simp add: F_Q(1) F_restriction_processptickI)
          qed
        qed
      qed
    qed
  qed
qed
   

declare Seqptick_restriction_shift_processptick
  [restriction_shift_processptick_simpset, simp]


text ‹The third one can be adapted for classical sequential composition.›

lemmas Seq_restriction_shift_processptick_3 =
  Seqptick_restriction_shift_processptick(3)[where g = ‹λx r. g x›, simplified] for g

declare Seq_restriction_shift_processptick_3 [restriction_shift_processptick_simpset, simp]




corollary MultiSeqptick_restriction_shift_processptick :
  ‹(⋀l. l ∈ set L ⟹ non_destructive (f l)) ⟹ non_destructive (λx. (SEQ✓ l ∈@ L. f l x) r)›
  ‹(⋀l. l ∈ set L ⟹ constructive (f l)) ⟹ constructive (λx. (SEQ✓ l ∈@ L. f l x) r)›
  ‹(case L of [] ⇒ True | l0 # L' ⇒
    constructive (f l0) ∧ (∀x r'. ✓(r') ∉ (f l0 x r)0) ∧ (∀l∈set L'. non_destructive (f l)))
    ⟹ constructive (λx. (SEQ✓ l ∈@ L. f l x) r)›
proof -
  show ‹(⋀l. l ∈ set L ⟹ constructive (f l)) ⟹ constructive (λx. (SEQ✓ l ∈@ L. f l x) r)›
    by (induct L arbitrary: r; simp add: constructive_fun_iff)
next
  show * : ‹(⋀l. l ∈ set L ⟹ non_destructive (f l)) ⟹
            non_destructive (λx. (SEQ✓ l ∈@ L. f l x) r)› for L r
    by (induct L arbitrary: r; simp add: non_destructive_fun_iff)

  show ‹(case L of [] ⇒ True | l0 # L' ⇒
        constructive (f l0) ∧ (∀x r'. ✓(r') ∉ (f l0 x r)0) ∧ (∀l∈set L'. non_destructive (f l)))
        ⟹ constructive (λx. (SEQ✓ l ∈@ L. f l x) r)›
    by (auto split: list.split_asm intro: Seqptick_restriction_shift_processptick(3)
        simp add: constructive_fun_iff non_destructive_fun_iff "*" )
qed


corollary MultiSeqptick_non_destructive :
  ‹non_destructive (λP. (SEQ✓ l ∈@ L. P l) r)›
  ‹non_destructive (λP. (SEQ✓ l ∈@ L. P l))›
  by (simp_all add: MultiSeqptick_restriction_shift_processptick(1)[of L ‹λl x. x l›])


declare MultiSeqptick_restriction_shift_processptick
  [restriction_shift_processptick_simpset, simp]



(*<*)
end
  (*>*)