Theory Compactification_Sequential_Composition_Generalized

(***********************************************************************************
 * 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
 ***********************************************************************************)


chapter ‹Compactification of Sequential Composition Generalized ›

(*<*)
theory Compactification_Sequential_Composition_Generalized
  imports Combining_Sequential_Composition_Generalized
begin
  (*>*)


section ‹Iterated Combine›

subsection ‹Definitions›

fun iterated_combined_Seqptick :: ‹[('r ⇒ ('σ, 'e, 'r) Ad) list, 'r] ⇒ ('σ list, 'e, 'r) Ad› (‹⟪d⨂;✓ _⟫› [0])
  where ‹⟪d⨂;✓ []⟫ r = ⦇τ = λσs a. ◇, ω = λσs. ⌊r⌋⦈›
  |     ‹⟪d⨂;✓ [A0]⟫ r = d⟪A0 r⟫σ↪σs›
  |     ‹⟪d⨂;✓ A0 # A1 # As⟫ r = ⟪A0 r d⊗;✓Rlist ⟪d⨂;✓ A1 # As⟫⟫›

fun iterated_combinend_Seqptick :: ‹[('r ⇒ ('σ, 'e, 'r) And) list, 'r] ⇒ ('σ list, 'e, 'r) And› (‹⟪nd⨂;✓ _⟫› [0])
  where ‹⟪nd⨂;✓ []⟫ r = ⦇τ = λσs a. {}, ω = λσs. {r}⦈›
  |     ‹⟪nd⨂;✓ [A0]⟫ r = nd⟪A0 r⟫σ↪σs›
  |     ‹⟪nd⨂;✓ A0 # A1 # As⟫ r = ⟪A0 r nd⊗;✓Rlist ⟪nd⨂;✓ A1 # As⟫⟫›


lemma iterated_combined_Seqptick_simps_bis: ‹As ≠ [] ⟹ ⟪d⨂;✓ A0 # As⟫ r = ⟪A0 r d⊗;✓Rlist ⟪d⨂;✓ As⟫⟫›
  and iterated_combinend_Seqptick_simps_bis: ‹Bs ≠ [] ⟹ ⟪nd⨂;✓ B0 # Bs⟫ r = ⟪B0 r nd⊗;✓Rlist ⟪nd⨂;✓ Bs⟫⟫›
  by (induct As, simp_all) (induct Bs, simp_all)



subsection ‹First Results›

lemma combineListslenL_Seqptick_combineRlist_Seqptick_eq:
  ‹ε ⟪d⟪A0⟫σ↪σs d⊗1;ListslenL A1⟫ (s0 # σs) = ε ⟪A0 d⊗;✓Rlist A1⟫ (s0 # σs)›
  ‹τ ⟪d⟪A0⟫σ↪σs d⊗1;ListslenL A1⟫ (s0 # σs) e = τ ⟪A0 d⊗;✓Rlist A1⟫ (s0 # σs) e›
  ‹ε ⟪nd⟪B0⟫σ↪σs nd⊗1;ListslenL B1⟫ (s0 # σs) = ε ⟪B0 nd⊗;✓Rlist B1⟫ (s0 # σs)›
  ‹τ ⟪nd⟪B0⟫σ↪σs nd⊗1;ListslenL B1⟫ (s0 # σs) e = τ ⟪B0 nd⊗;✓Rlist B1⟫ (s0 # σs) e›
  by (simp_all add: ε_simps ρ_simps combineListslenL_Seqptick combineRlist_Seqptick_defs σ_σs_conv_defs)
    (safe, auto simp add: map_option_case split: option.splits)


lemma combinePairlist_Seqptick_and_iterated_combine_Seqptick_eq:
  ‹ε ⟪A0 r d⊗;✓Pairlist A1⟫ [s0, s1] = ε (⟪d⨂;✓ [A0, A1]⟫ r) [s0, s1]›
  ‹τ ⟪A0 r d⊗;✓Pairlist A1⟫ [s0, s1] e = τ (⟪d⨂;✓ [A0, A1]⟫ r) [s0, s1] e›
  ‹ε ⟪B0 r nd⊗;✓Pairlist B1⟫ [s0, s1] = ε (⟪nd⨂;✓ [B0, B1]⟫ r) [s0, s1]›
  ‹τ ⟪B0 r nd⊗;✓Pairlist B1⟫ [s0, s1] e = τ (⟪nd⨂;✓ [B0, B1]⟫ r) [s0, s1] e›
  by (simp_all add: ε_simps ρ_simps combinePairlist_Seqptick_defs combineRlist_Seqptick_defs σ_σs_conv_defs)
    (safe, auto simp add: map_option_case split: option.splits)


lemma combinePairlist_Seqptick_and_combineRlist_Seqptick_eq :
  ‹ε ⟪A0 d⊗;✓Pairlist A1⟫ [s0, s1] = ε ⟪A0 d⊗;✓Rlist ⟪d⨂;✓ [A1]⟫⟫ [s0, s1]›
  ‹τ ⟪A0 d⊗;✓Pairlist A1⟫ [s0, s1] e = τ ⟪A0 d⊗;✓Rlist ⟪d⨂;✓ [A1]⟫⟫ [s0, s1] e›
  ‹ε ⟪B0 nd⊗;✓Pairlist B1⟫ [s0, s1] = ε ⟪B0 nd⊗;✓Rlist ⟪nd⨂;✓ [B1]⟫⟫ [s0, s1]›
  ‹τ ⟪B0 nd⊗;✓Pairlist B1⟫ [s0, s1] e = τ ⟪B0 nd⊗;✓Rlist ⟪nd⨂;✓ [B1]⟫⟫ [s0, s1] e›
  by (simp_all add: ε_simps ρ_simps combinePairlist_Seqptick_defs combineRlist_Seqptick_defs σ_σs_conv_defs)
    (safe, auto simp add: map_option_case split: option.splits)



subsection ‹Reachability›

lemma same_length_τ_iterated_combined_Seqptick :
  ‹length σs = length As ⟹ ⌊σt⌋ = τ (⟪d⨂;✓ As⟫ r) σs a ⟹ length σt = length As›
proof (induct arbitrary: σt r rule: induct_2_lists012)
  case Nil thus ?case by simp
next
  case (single σ0 A0) thus ?case
    by simp (metis length_1_transdE length_1_trans_from_σ_to_σs(1) length_Cons list.size(3))
next
  case (Cons σ0 σ1 σs A0 A1 As)
  from Cons.prems Cons.hyps(1, 3) show ?case
    by (simp add: combineRlist_Seqptick_defs map_option_case ρ_simps
        split: if_split_asm option.split_asm) metis
qed

lemma same_length_τ_iterated_combinend_Seqptick :
  ‹length σs = length As ⟹ σt ∈ τ (⟪nd⨂;✓ As⟫ r) σs a ⟹ length σt = length As›
proof (induct arbitrary: σt r rule: induct_2_lists012)
  case Nil thus ?case by simp
next
  case (single σ0 A0) thus ?case
    by simp (meson length_1_transnd_def length_1_trans_from_σ_to_σs(2))
next
  case (Cons σ0 σ1 σs A0 A1 As)
  from Cons.prems Cons.hyps(1, 3) show ?case
    by (auto simp add: combineRlist_Seqptick_defs map_option_case ρ_simps
        split: if_split_asm)
qed



lemma same_length_ℛd_iterated_combined_Seqptick :
  ‹σt ∈ ℛd (⟪d⨂;✓ As⟫ r) σs ⟹ length σs = length As ⟹ length σt = length As›
  by (induct rule: ℛd.induct, simp) (meson same_length_τ_iterated_combined_Seqptick)

lemma same_length_ℛnd_iterated_combinend_Seqptick :
  ‹σt ∈ ℛnd (⟪nd⨂;✓ As⟫ r) σs ⟹ length σs = length As ⟹ length σt = length As›
  by (induct rule: ℛnd.induct, simp) (meson same_length_τ_iterated_combinend_Seqptick)



subsection ‹Transmission of Properties›

lemma ρ_disjoint_ε_transmission_to_iterated_combine_Seqptick :
  ‹As ≠ [] ⟹ ρ_disjoint_ε ((last As) r) ⟹ ρ_disjoint_ε (⟪d⨂;✓ As⟫ r)›
  ‹Bs ≠ [] ⟹ ρ_disjoint_ε ((last Bs) r) ⟹ ρ_disjoint_ε (⟪nd⨂;✓ Bs⟫ r)›
  by (induct rule: induct_list012;
      auto simp add: ρ_disjoint_ε_def combineRlist_Seqptick_defs ε_simps ρ_simps σ_σs_conv_defs)+



subsection ‹Normalization›

lemma ω_iterated_combine_Seqptick_det_ndet_conv:
  ‹ω (⟪nd⨂;✓ map (λA r. ⟪A r⟫d↪nd) As⟫ r) σs = ω ⟪⟪d⨂;✓ As⟫ r⟫d↪nd σs›
  by (induct As arbitrary: σs r rule: induct_list012[case_names Nil singl Cons])
    (simp_all add: from_det_to_ndet_σ_σs_conv_commute combineRlist_Seqptick_defs
      ω_from_det_to_ndet split: option.split)

lemma ρ_iterated_combine_Seqptick_det_ndet_conv :
  ‹ρ (⟪nd⨂;✓ map (λA r. ⟪A r⟫d↪nd) As⟫ r) = ρ ⟪⟪d⨂;✓ As⟫ r⟫d↪nd›
  by (simp add: ρ_simps ω_iterated_combine_Seqptick_det_ndet_conv)


lemma τ_iterated_combine_Seqptick_behaviour:
  ‹length σs = length As ⟹
   τ ⟪⟪d⨂;✓ As⟫ r⟫d↪nd σs e = τ (⟪nd⨂;✓ map (λA r. ⟪A r⟫d↪nd) As⟫ r) σs e›
proof (induct σs As arbitrary: r rule: induct_2_lists012)
  case Nil show ?case by simp
next
  case (single σ0 A0)
  show ?case by (simp add: from_det_to_ndet_σ_σs_conv_commute(1))
next
  case (Cons σ0 σ1 σs A0 A1 As)
  show ?case
    by (simp add: τ_combineRlist_Seqptick_behaviour split: option.split,
        simp add: combineRlist_Seqptick_defs ρ_iterated_combine_Seqptick_det_ndet_conv
        ω_from_det_to_ndet split: option.split)
      (metis Cons.hyps(3) ρ_iterated_combine_Seqptick_det_ndet_conv det_ndet_conv_ρ(1) list.simps(9))
qed



lemma PSKIPS_iterated_combine_Seqptick_behaviour:
  assumes same_length: ‹length σs = length As›
  shows ‹PSKIPS⟪⟪d⨂;✓ As⟫ r⟫d σs = PSKIPS⟪⟪nd⨂;✓ map (λA r. ⟪A r⟫d↪nd) As⟫ r⟫nd σs›
proof (fold PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d, rule PSKIPS_nd_eqI_strong_id)
  show ‹σt ∈ ℛnd ⟪⟪d⨂;✓ As⟫ r⟫d↪nd σs ⟹
        τ (⟪nd⨂;✓ map (λA r. ⟪A r⟫d↪nd) As⟫ r) σt a = τ ⟪⟪d⨂;✓ As⟫ r⟫d↪nd σt a› for σt a
    by (simp add: ℛnd_from_det_to_ndet τ_iterated_combine_Seqptick_behaviour
        same_length same_length_ℛd_iterated_combined_Seqptick)
next
  show ‹ω (⟪nd⨂;✓ map (λA r. ⟪A r⟫d↪nd) As⟫ r) σt = ω ⟪⟪d⨂;✓ As⟫ r⟫d↪nd σt› for σt
    by (simp add: ω_iterated_combine_Seqptick_det_ndet_conv)
qed

lemma P_iterated_combine_Seqptick_behaviour:
  assumes same_length: ‹length σs = length As›
  shows ‹P⟪⟪d⨂;✓ As⟫ r⟫d σs = P⟪⟪nd⨂;✓ map (λA r. ⟪A r⟫d↪nd) As⟫ r⟫nd σs›
proof (fold P_nd_from_det_to_ndet_is_P_d, rule P_nd_eqI_strong_id)
  show ‹σt ∈ ℛnd ⟪⟪d⨂;✓ As⟫ r⟫d↪nd σs ⟹
       τ (⟪nd⨂;✓ map (λA r. ⟪A r⟫d↪nd) As⟫ r) σt a = τ ⟪⟪d⨂;✓ As⟫ r⟫d↪nd σt a› for σt a
    by (simp add: ℛnd_from_det_to_ndet τ_iterated_combine_Seqptick_behaviour
        same_length same_length_ℛd_iterated_combined_Seqptick)
qed



section ‹Compactification Theorems›

subsection ‹Binary›

subsubsection ‹Pair›

lemma PSKIPS_nd_combinePair_Seqptick :
  fixes A0 A1
  assumes at_most_1_elem_term : ‹at_most_1_elem_term A0›
    ― ‹This assumption is necessary in the new setup,
        otherwise the result is not always a Procomaton
        (for example if term‹ω A0 σ0 = UNIV›,
         we have term‹P σ0 ;✓ Q σ1 = ⊓r∈UNIV. Q σ1 r›).›
    (* TODO: weaken this to reachable terminations ? *)
  defines A_def: ‹A ≡ ⟪A0 nd⊗;✓Pair A1⟫› 
  defines P_def: ‹P ≡ PSKIPS⟪A0⟫nd›
    and Q_def: ‹Q ≡ λσ1 r. PSKIPS⟪A1 r⟫nd σ1›
    and S_def: ‹S ≡ PSKIPS⟪A⟫nd›
  shows ‹P σ0 ;✓ Q σ1 = S (σ0, σ1)›
proof -
  let ?f = ‹PSKIPS_nd_step (ε A) (τ A) (ω A) (λσ'. case σ' of (σ0, σ1) ⇒ P σ0 ;✓ Q σ1)›
  note cartprod_rwrt = GlobalNdet_cartprod[of _ _ ‹λx y. _ (x, y)›, simplified]
  note Ndet_and_Seq = Seqptick_distrib_GlobalNdet_left Seqptick_distrib_GlobalNdet_right
  have P_rec : ‹P σ0 = PSKIPS_nd_step (ε A0) (τ A0) (ω A0) P σ0› for σ0
    by (fact restriction_fix_eq[OF PSKIPS_nd_step_constructive_bis[of A0],
          folded PSKIPS_nd_def P_def, THEN fun_cong])
  have Q_rec : ‹Q σ1 = (λr. PSKIPS_nd_step (ε (A1 r)) (τ (A1 r)) (ω (A1 r)) (λσ1. Q σ1 r) σ1)› for σ1
    by (rule ext, simp add: Q_def PSKIPS_nd_rec)
  show ‹P σ0 ;✓ Q σ1 = S (σ0, σ1)›
  proof (rule fun_cong[of ‹λ(σ0, σ1).P σ0 ;✓ Q σ1› _ ‹(σ0, σ1)›, simplified])
    show ‹(λ(σ0, σ1). P σ0 ;✓ Q σ1) = S›
    proof (rule restriction_fix_unique[OF PSKIPS_nd_step_constructive_bis[of A],
          symmetric, folded PSKIPS_nd_def S_def])
      show ‹?f = (λ(σ0, σ1). P σ0 ;✓ Q σ1)›
      proof (rule ext, clarify)
        show ‹?f (σ0, σ1) = P σ0 ;✓ Q σ1› for σ0 σ1
        proof (cases ‹σ0 ∈ ρ A0›)
          show ‹σ0 ∉ ρ A0 ⟹ ?f (σ0, σ1) = P σ0 ;✓ Q σ1›
            by (subst (2) P_rec)
              (auto simp add: combinePair_Seqptick_defs ε_simps A_def ρ_simps
                Mprefix_Seqptick cartprod_rwrt Ndet_and_Seq intro!: mono_Mprefix_eq)
        next
          assume ‹σ0 ∈ ρ A0›
          hence ‹ω A0 σ0 ≠ {}› by (simp add: ρ_simps)
          then obtain r where ‹ω A0 σ0 = {r}›
            by (meson at_most_1_elem_term at_most_1_elem_termE)
          from ‹σ0 ∈ ρ A0› have P_rec' : ‹P σ0 = SKIPS (ω A0 σ0)› by (simp add: P_rec ρ_simps)
          have ε_A : ‹ε A (σ0, σ1) = (if σ1 ∈ ρ (A1 r) then {} else ε (A1 r) σ1)›
            by (simp add: A_def ε_combinePair_Seqptick combine_Seq_ε_defs ‹σ0 ∈ ρ A0› ‹ω A0 σ0 = {r}›)
          from ‹σ0 ∈ ρ A0› have ω_A : ‹ω A (σ0, σ1) = ω (A1 r) σ1›
            by (simp add: A_def combinePair_Seqptick_defs ‹ω A0 σ0 = {r}›)
          show ‹?f (σ0, σ1) = P σ0 ;✓ Q σ1›
          proof (cases ‹σ1 ∈ ρ (A1 r)›)
            show ‹σ1 ∈ ρ (A1 r) ⟹ ?f (σ0, σ1) = P σ0 ;✓ Q σ1›
              by (subst (2) Q_rec)
                (simp add: P_rec' ε_A ω_A SKIPS_def Ndet_and_Seq ‹ω A0 σ0 = {r}› ρ_simps)
          next
            show ‹σ1 ∉ ρ (A1 r) ⟹ ?f (σ0, σ1) = P σ0 ;✓ Q σ1›
              by (subst (2) Q_rec, unfold ε_A ω_A SKIPS_def)
                (auto simp add: A_def P_rec' Ndet_and_Seq ‹ω A0 σ0 = {r}›
                  ρ_simps cartprod_rwrt combinePair_Seqptick_defs intro!: mono_Mprefix_eq)
          qed
        qed
      qed
    qed
  qed
qed

corollary PSKIPS_d_combinePair_Seqptick :
  ‹PSKIPS⟪A0⟫d σ0 ;✓ (λr. PSKIPS⟪A1 r⟫d σ1) = PSKIPS⟪⟪A0 d⊗;✓Pair A1⟫⟫d (σ0, σ1)›
proof -
  have ‹PSKIPS⟪A0⟫d σ0 ;✓ (λr. PSKIPS⟪A1 r⟫d σ1) =
        PSKIPS⟪⟪A0⟫d↪nd⟫nd σ0 ;✓ (λr. PSKIPS⟪⟪A1 r⟫d↪nd⟫nd σ1)›
    by (simp add: PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d)
  also have ‹… = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗;✓Pair (λr. ⟪A1 r⟫d↪nd)⟫⟫nd (σ0, σ1)›
    by (metis PSKIPS_nd_combinePair_Seqptick at_most_1_elem_from_det_to_ndet
        at_most_1_elem_imp_at_most_1_elem_term)
  also have ‹… = PSKIPS⟪⟪A0 d⊗;✓Pair A1⟫⟫d (σ0, σ1)›
    by (simp add: PSKIPS_combinePair_Seqptick_behaviour)
  finally show ?thesis .
qed



subsubsection ‹Pairlist›

lemma PSKIPS_nd_combinePairlist_Seqptick :
  ‹PSKIPS⟪A0⟫nd σ0 ;✓ (λr. PSKIPS⟪A1 r⟫nd σ1) = PSKIPS⟪⟪A0 nd⊗;✓Pairlist A1⟫⟫nd [σ0, σ1]›
  if ‹at_most_1_elem_term A0›
proof -
  from PSKIPS_nd_combinePair_Seqptick[OF ‹at_most_1_elem_term A0›]
  have ‹PSKIPS⟪A0⟫nd σ0 ;✓ (λr. PSKIPS⟪A1 r⟫nd σ1) =
        PSKIPS⟪⟪A0 nd⊗;✓Pair A1⟫⟫nd (σ0, σ1)› .
  also have ‹… = PSKIPS⟪⟪A0 nd⊗;✓Pairlist A1⟫⟫nd [σ0, σ1]›
  proof (rule PSKIPS_nd_eqI_strong[of ‹λ(σ0, σ1). [σ0, σ1]› _ ‹(σ0, σ1)›, simplified])
    show ‹inj_on (λ(σ0, σ1). [σ0, σ1]) (ℛnd ⟪A0 nd⊗;✓Pair A1⟫ (σ0, σ1))›
      by (auto intro: inj_onI)
  next
    show ‹τ ⟪A0 nd⊗;✓Pairlist A1⟫ (case σ' of (σ0, σ1) ⇒ [σ0, σ1]) a =
          (λσ'. case σ' of (σ0, σ1) ⇒ [σ0, σ1]) ` τ ⟪A0 nd⊗;✓Pair A1⟫ σ' a› for σ' a
      by (cases σ') (auto simp add: combinePair_Seqptick_defs combinePairlist_Seqptick_defs)
  next
    show ‹ω ⟪A0 nd⊗;✓Pairlist A1⟫ (case σ' of (σ0, σ1) ⇒ [σ0, σ1]) = ω ⟪A0 nd⊗;✓Pair A1⟫ σ'› for σ'
      by (cases σ') (auto simp add: combinePair_Seqptick_defs combinePairlist_Seqptick_defs)
  qed
  finally show ?thesis .
qed

corollary PSKIPS_d_combinePairlist_Seqptick :
  ‹PSKIPS⟪A0⟫d σ0 ;✓ (λr. PSKIPS⟪A1 r⟫d σ1) = PSKIPS⟪⟪A0 d⊗;✓Pairlist A1⟫⟫d [σ0, σ1]›
proof -
  have ‹PSKIPS⟪A0⟫d σ0 ;✓ (λr. PSKIPS⟪A1 r⟫d σ1) =
        PSKIPS⟪⟪A0⟫d↪nd⟫nd σ0 ;✓ (λr. PSKIPS⟪⟪A1 r⟫d↪nd⟫nd σ1)›
    by (simp add: PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d)
  also have ‹… = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗;✓Pairlist (λr. ⟪A1 r⟫d↪nd)⟫⟫nd [σ0, σ1]›
    by (metis PSKIPS_nd_combinePairlist_Seqptick at_most_1_elem_from_det_to_ndet
        at_most_1_elem_imp_at_most_1_elem_term)
  also have ‹… = PSKIPS⟪⟪A0 d⊗;✓Pairlist A1⟫⟫d [σ0, σ1]›
    by (simp add: PSKIPS_combinePairlist_Seqptick_behaviour)
  finally show ?thesis .
qed



subsubsection ‹Rlist›

lemma PSKIPS_nd_combineRlist_Seqptick :
  ‹PSKIPS⟪A0⟫nd σ0 ;✓ (λr. PSKIPS⟪A1 r⟫nd σs) = PSKIPS⟪⟪A0 nd⊗;✓Rlist A1⟫⟫nd (σ0 # σs)›
  if ‹at_most_1_elem_term A0›
proof -
  from PSKIPS_nd_combinePair_Seqptick[OF ‹at_most_1_elem_term A0›]
  have ‹PSKIPS⟪A0⟫nd σ0 ;✓ (λr. PSKIPS⟪A1 r⟫nd σs) =
        PSKIPS⟪⟪A0 nd⊗;✓Pair A1⟫⟫nd (σ0, σs)› .
  also have ‹… = PSKIPS⟪⟪A0 nd⊗;✓Rlist A1⟫⟫nd (σ0 # σs)›
  proof (rule PSKIPS_nd_eqI_strong[of ‹λ(σ0, σs). σ0 # σs› _ ‹(σ0, σs)›, simplified])
    show ‹inj_on (λ(σ0, σs). σ0 # σs) (ℛnd ⟪A0 nd⊗;✓Pair A1⟫ (σ0, σs))›
      by (auto intro: inj_onI)
  next
    show ‹τ ⟪A0 nd⊗;✓Rlist A1⟫ (case σ' of (σ0, σs) ⇒ σ0 # σs) a =
         (λσ'. case σ' of (σ0, σs) ⇒ σ0 # σs) ` τ ⟪A0 nd⊗;✓Pair A1⟫ σ' a› for σ' a
      by (cases σ') (auto simp add: combinePair_Seqptick_defs combineRlist_Seqptick_defs)
  next
    show ‹ω ⟪A0 nd⊗;✓Rlist A1⟫ (case σ' of (σ0, σs) ⇒ σ0 # σs) = ω ⟪A0 nd⊗;✓Pair A1⟫ σ'› for σ'
      by (cases σ') (auto simp add: combinePair_Seqptick_defs combineRlist_Seqptick_defs)
  qed
  finally show ?thesis .
qed

corollary PSKIPS_d_combineRlist_Seqptick :
  ‹PSKIPS⟪A0⟫d σ0 ;✓ (λr. PSKIPS⟪A1 r⟫d σs) = PSKIPS⟪⟪A0 d⊗;✓Rlist A1⟫⟫d (σ0 # σs)›
proof -
  have ‹PSKIPS⟪A0⟫d σ0 ;✓ (λr. PSKIPS⟪A1 r⟫d σs) =
        PSKIPS⟪⟪A0⟫d↪nd⟫nd σ0 ;✓ (λr. PSKIPS⟪⟪A1 r⟫d↪nd⟫nd σs)›
    by (simp add: PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d)
  also have ‹… = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗;✓Rlist (λr. ⟪A1 r⟫d↪nd)⟫⟫nd (σ0 # σs)›
    by (metis PSKIPS_nd_combineRlist_Seqptick at_most_1_elem_from_det_to_ndet
        at_most_1_elem_imp_at_most_1_elem_term)
  also have ‹… = PSKIPS⟪⟪A0 d⊗;✓Rlist A1⟫⟫d (σ0 # σs)›
    by (simp add: PSKIPS_combineRlist_Seqptick_behaviour)
  finally show ?thesis .
qed



subsection ‹ListslenL›

lemma PSKIPS_nd_combineListslenL_Seqptick :
  ‹PSKIPS⟪A0⟫nd σs0 ;✓ (λr. PSKIPS⟪A1 r⟫nd σs1) = PSKIPS⟪⟪A0 nd⊗len0;ListslenL A1⟫⟫nd (σs0 @ σs1)›
  if same_length_reach : ‹⋀σs0'. σs0' ∈ ℛnd A0 σs0 ⟹ length σs0' = len0›
    and ‹at_most_1_elem_term A0›
proof -
  from PSKIPS_nd_combinePair_Seqptick[OF ‹at_most_1_elem_term A0›]
  have ‹PSKIPS⟪A0⟫nd σs0 ;✓ (λr. PSKIPS⟪A1 r⟫nd σs1) =
        PSKIPS⟪⟪A0 nd⊗;✓Pair A1⟫⟫nd (σs0, σs1)› .
  also have ‹… = PSKIPS⟪⟪A0 nd⊗len0;ListslenL A1⟫⟫nd (σs0 @ σs1)›
  proof (rule PSKIPS_nd_eqI_strong[of ‹λ(σs0, σs1). σs0 @ σs1› _ ‹(σs0, σs1)›, simplified])
    show ‹inj_on (λ(σs0, σs1). σs0 @ σs1) (ℛnd ⟪A0 nd⊗;✓Pair A1⟫ (σs0, σs1))›
    proof (rule inj_onI, clarify)
      fix σs0' σs1' σs0'' σs1''
      assume assms : ‹(σs0', σs1') ∈ ℛnd ⟪A0 nd⊗;✓Pair A1⟫ (σs0, σs1)›
        ‹(σs0'', σs1'') ∈ ℛnd ⟪A0 nd⊗;✓Pair A1⟫ (σs0, σs1)›
        ‹σs0' @ σs1' = σs0'' @ σs1''›
      from ℛnd_combinendPair_Seqptick_subset assms(1, 2)
      have ‹σs0' ∈ ℛnd A0 σs0› ‹σs0'' ∈ ℛnd A0 σs0› by fast+
      with same_length_reach have ‹length σs0' = length σs0''› by blast
      with assms(3) show ‹σs0' = σs0'' ∧ σs1' = σs1''› by simp
    qed
  next
    fix σs' a
    assume ‹σs' ∈ ℛnd ⟪A0 nd⊗;✓Pair A1⟫ (σs0, σs1)›
    with ℛnd_combinendPair_Seqptick_subset
    obtain σs0' σs1' where ‹σs' = (σs0', σs1')› ‹σs0' ∈ ℛnd A0 σs0› by fast
    from ‹σs0' ∈ ℛnd A0 σs0› same_length_reach have ‹length σs0' = len0› by blast
    show ‹τ ⟪A0 nd⊗len0;ListslenL A1⟫ (case σs' of (σs0, σs1) ⇒ σs0 @ σs1) a =
          (λσs'. case σs' of (σs0, σs1) ⇒ σs0 @ σs1) ` τ ⟪A0 nd⊗;✓Pair A1⟫ σs' a›
      by (auto simp add: ‹σs' = (σs0', σs1')› ‹length σs0' = len0›
          combinePair_Seqptick_defs combineListslenL_Seqptick)
  next
    fix σs' a
    assume ‹σs' ∈ ℛnd ⟪A0 nd⊗;✓Pair A1⟫ (σs0, σs1)›
    with ℛnd_combinendPair_Seqptick_subset
    obtain σs0' σs1' where ‹σs' = (σs0', σs1')› ‹σs0' ∈ ℛnd A0 σs0› by fast
    from ‹σs0' ∈ ℛnd A0 σs0› same_length_reach have ‹length σs0' = len0› by blast
    show ‹ω ⟪A0 nd⊗len0;ListslenL A1⟫ (case σs' of (σs0, σs1) ⇒ σs0 @ σs1) = ω ⟪A0 nd⊗;✓Pair A1⟫ σs'›
      by (auto simp add: ‹σs' = (σs0', σs1')› ‹length σs0' = len0›
          combinePair_Seqptick_defs combineListslenL_Seqptick)
  qed
  finally show ?thesis .
qed


corollary PSKIPS_d_combineListslenL_Seqptick :
  ‹PSKIPS⟪A0⟫d σs0 ;✓ (λr. PSKIPS⟪A1 r⟫d σs1) = PSKIPS⟪⟪A0 d⊗len0;ListslenL A1⟫⟫d (σs0 @ σs1)›
  if same_length_reach : ‹⋀σs0'. σs0' ∈ ℛd A0 σs0 ⟹ length σs0' = len0›
proof -
  have ‹PSKIPS⟪A0⟫d σs0 ;✓ (λr. PSKIPS⟪A1 r⟫d σs1) =
        PSKIPS⟪⟪A0⟫d↪nd⟫nd σs0 ;✓ (λr. PSKIPS⟪⟪A1 r⟫d↪nd⟫nd σs1)›
    by (simp add: PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d)
  also have ‹… = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗len0;ListslenL (λr. ⟪A1 r⟫d↪nd)⟫⟫nd (σs0 @ σs1)›
    by (rule PSKIPS_nd_combineListslenL_Seqptick[OF same_length_reach])
      (simp_all add: ℛnd_from_det_to_ndet at_most_1_elem_imp_at_most_1_elem_term)
  also have ‹… = PSKIPS⟪⟪A0 d⊗len0;ListslenL A1⟫⟫d (σs0 @ σs1)›
    by (simp add: PSKIPS_combineListslenL_Seqptick_behaviour same_length_reach)
  finally show ?thesis .
qed



subsection ‹Multiple›

theorem PSKIPS_nd_compactification_Seqptick:
  ‹⟦length σs = length As; ⋀A r. A ∈ set (butlast As) ⟹ at_most_1_elem_term (A r)⟧ ⟹
   SEQ✓ (σ, A) ∈@ zip σs As. (λr. PSKIPS⟪A r⟫nd σ) = (λr. PSKIPS⟪⟪nd⨂;✓ As⟫ r⟫nd σs)›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by (simp add: PSKIPS_nd_rec)
next
  case (single σ0 A0) show ?case by (simp add: PSKIPS_nd_from_σ_to_σs_is_PSKIPS_nd)
next
  case (Cons σ0 σ1 σs A0 A1 As)
  have ‹SEQ✓ (σ, A) ∈@ zip (σ0 # σ1 # σs) (A0 # A1 # As). (λr. PSKIPS⟪A r⟫nd σ) =
        (λr. PSKIPS⟪A0 r⟫nd σ0 ;✓ SEQ✓ (σ, A) ∈@ zip (σ1 # σs) (A1 # As). (λr. PSKIPS⟪A r⟫nd σ))› by simp
  also have ‹SEQ✓ (σ, A) ∈@ zip (σ1 # σs) (A1 # As). (λr. PSKIPS⟪A r⟫nd σ) =
             (λr. PSKIPS⟪⟪nd⨂;✓ A1 # As⟫ r⟫nd (σ1 # σs))›
    by (rule Cons.hyps(3)) (simp add: Cons.prems)
  also have ‹(λr. PSKIPS⟪A0 r⟫nd σ0 ;✓ (λr. PSKIPS⟪⟪nd⨂;✓ A1 # As ⟫ r⟫nd (σ1 # σs))) =
             (λr. PSKIPS⟪⟪A0 r nd⊗;✓Rlist ⟪nd⨂;✓ A1 # As⟫⟫⟫nd (σ0 # σ1 # σs))›
    by (intro ext PSKIPS_nd_combineRlist_Seqptick) (simp add: Cons.prems)
  also have ‹… = (λr. PSKIPS⟪⟪nd⨂;✓ A0 # A1 # As⟫ r⟫nd (σ0 # σ1 # σs))› by simp
  finally show ?case .
qed

corollary PSKIPS_d_compactification_Seqptick:
  ‹length σs = length As ⟹
   SEQ✓ (σ, A) ∈@ zip σs As. (λr. PSKIPS⟪A r⟫d σ) = (λr. PSKIPS⟪⟪d⨂;✓ As⟫ r⟫d σs)›
proof (induct σs As rule: induct_2_lists012)
  case Nil show ?case by (simp add: PSKIPS_d_rec)
next
  case (single σ0 A0) show ?case by (simp add: PSKIPS_d_from_σ_to_σs_is_PSKIPS_d)
next
  case (Cons σ0 σ1 σs A0 A1 As)
  have ‹SEQ✓ (σ, A) ∈@ zip (σ0 # σ1 # σs) (A0 # A1 # As). (λr. PSKIPS⟪A r⟫d σ) =
        (λr. PSKIPS⟪A0 r⟫d σ0 ;✓ SEQ✓ (σ, A) ∈@ zip (σ1 # σs) (A1 # As). (λr. PSKIPS⟪A r⟫d σ))› by simp
  also have ‹SEQ✓ (σ, A) ∈@ zip (σ1 # σs) (A1 # As). (λr. PSKIPS⟪A r⟫d σ) =
             (λr. PSKIPS⟪⟪d⨂;✓ A1 # As⟫ r⟫d (σ1 # σs))›
    by (fact Cons.hyps(3))
  also have ‹(λr. PSKIPS⟪A0 r⟫d σ0 ;✓ (λr. PSKIPS⟪⟪d⨂;✓ A1 # As⟫ r⟫d (σ1 # σs))) =
             (λr. PSKIPS⟪⟪A0 r d⊗;✓Rlist ⟪d⨂;✓ A1 # As⟫⟫⟫d (σ0 # σ1 # σs))›
    by (intro ext PSKIPS_d_combineRlist_Seqptick)
  also have ‹… = (λr. PSKIPS⟪⟪d⨂;✓ A0 # A1 # As⟫ r⟫d (σ0 # σ1 # σs))› by simp
  finally show ?case .
qed



(*<*)
end
  (*>*)