Theory Combining_Synchronization_Product

(***********************************************************************************
 * 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 ‹Combining Automata for Synchronization Product›

(*<*)
theory Combining_Synchronization_Product
  imports Process_Normalization
begin
  (*>*)


section ‹Definitions›

subsection ‹General Patterns›

abbreviation combine_sets_Sync :: ‹'a set ⇒ 'a set ⇒ 'a set ⇒ 'a set›
  where ‹combine_sets_Sync S0 E S1 ≡ (S0 - E - S1) ∪ (S1 - E - S0) ∪ (S0 ∩ S1 - E) ∪ S0 ∩ S1 ∩ E›

definition combine_Sync_ε :: 
  ‹[('σ0, 'e, 'σ0', 'r0, 'α0) A_scheme, 'e set,
    ('σ1, 'e, 'σ1', 'r1, 'α1) A_scheme, 'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'σ] ⇒ 'e set›
  where ‹combine_Sync_ε A0 E A1 i0 i1 σs ≡ combine_sets_Sync (ε A0 (i0 σs)) E (ε A1 (i1 σs))›

lemma combine_Sync_ε_def_bis :
  ‹combine_Sync_ε A0 E A1 i0 i1 σs =
   ε A0 (i0 σs) ∪ ε A1 (i1 σs) - E ∪ ε A0 (i0 σs) ∩ ε A1 (i1 σs)›
  by (auto simp add: combine_Sync_ε_def)


fun combined_Sync_τ :: 
  ‹[('σ0, 'e, 'r0, 'α0) Ad_scheme, 'e set, ('σ1, 'e, 'r1, 'α1) Ad_scheme,
    'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'σ0 ⇒ 'σ1 ⇒ 'σ] ⇒ ('σ, 'e) transd›
  and combinend_Sync_τ ::
  ‹[('σ0, 'e, 'r0, 'α0) And_scheme, 'e set, ('σ1, 'e, 'r1, 'α1) And_scheme,
     'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'σ0 ⇒ 'σ1 ⇒ 'σ] ⇒ ('σ, 'e) transnd›
  where ‹combined_Sync_τ  A0 E A1 i0 i1 f σs e =
         (       if e ∈ ε A0 (i0 σs) ∩ ε A1 (i1 σs)
               then update_both  A0 A1 (i0 σs) (i1 σs) e (f_up_opt f)
          else   if e ∈ ε A0 (i0 σs) - E - ε A1 (i1 σs)
               then update_left  A0    (i0 σs) (i1 σs) e (f_up_opt f) (λs. ⌊s⌋)
          else   if e ∈ ε A1 (i1 σs) - E - ε A0 (i0 σs)
               then update_right    A1 (i0 σs) (i1 σs) e (f_up_opt f) (λs. ⌊s⌋)
          else      ◇)›
  |     ‹combinend_Sync_τ  A0 E A1 i0 i1 f σs e = 
         (       if e ∈ ε A0 (i0 σs) ∩ ε A1 (i1 σs) ∩ E
               then update_both  A0 A1 (i0 σs) (i1 σs) e (f_up_set f)
          else   if e ∈ ε A0 (i0 σs) ∩ ε A1 (i1 σs) - E
               then update_left  A0    (i0 σs) (i1 σs) e (f_up_set f) (λs. {s})
                  ∪ update_right    A1 (i0 σs) (i1 σs) e (f_up_set f) (λs. {s})
          else   if e ∈ ε A0 (i0 σs) - E - ε A1 (i1 σs)
               then update_left  A0    (i0 σs) (i1 σs) e (f_up_set f) (λs. {s})
          else   if e ∈ ε A1 (i1 σs) - E - ε A0 (i0 σs)
               then update_right    A1 (i0 σs) (i1 σs) e (f_up_set f) (λs. {s})
          else      {})›

fun combined_Sync_ω :: 
  ‹[('σ0, 'e, 'r0, 'α0) Ad_scheme, 'e set, ('σ1, 'e, 'r1, 'α1) Ad_scheme,
    'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'r0 ⇒ 'r1 ⇒ 'r option] ⇒ ('σ ⇒ 'r option)›
  and combinend_Sync_ω ::
  ‹[('σ0, 'e, 'r0, 'α0) And_scheme, 'e set, ('σ1, 'e, 'r1, 'α1) And_scheme,
     'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'r0 ⇒ 'r1 ⇒ 'r option] ⇒ ('σ ⇒ 'r set)›
  where ‹combined_Sync_ω A0 E A1 i0 i1 g σs =
         (case ω A0 (i0 σs)
            of ◇ ⇒ ◇ | ⌊r0⌋ ⇒ (case ω A1 (i1 σs) of ◇ ⇒ ◇ | ⌊r1⌋ ⇒ g r0 r1))›
  |     ‹combinend_Sync_ω A0 E A1 i0 i1 g σs =
         {r |r r0 r1. g r0 r1 = ⌊r⌋ ∧ r0 ∈ ω A0 (i0 σs) ∧ r1 ∈ ω A1 (i1 σs)}›

fun combined_Sync :: 
  ‹[('σ0, 'e, 'r0, 'α0) Ad_scheme, 'e set, ('σ1, 'e, 'r1, 'α1) Ad_scheme,
    'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'σ0 ⇒ 'σ1 ⇒ 'σ, 'r0 ⇒ 'r1 ⇒ 'r option] ⇒ ('σ, 'e, 'r) Ad›
  and combinend_Sync ::
  ‹[('σ0, 'e, 'r0, 'α0) And_scheme, 'e set, ('σ1, 'e, 'r1, 'α1) And_scheme,
     'σ ⇒ 'σ0, 'σ ⇒ 'σ1, 'σ0 ⇒ 'σ1 ⇒ 'σ, 'r0 ⇒ 'r1 ⇒ 'r option] ⇒ ('σ, 'e, 'r) And›
  where ‹combined_Sync A0 E A1 i0 i1 f g = 
         ⦇τ = combined_Sync_τ A0 E A1 i0 i1 f, ω = combined_Sync_ω A0 E A1 i0 i1 g⦈›
  |     ‹combinend_Sync A0 E A1 i0 i1 f g = 
         ⦇τ = combinend_Sync_τ A0 E A1 i0 i1 f, ω = combinend_Sync_ω A0 E A1 i0 i1 g⦈›



subsection ‹Specializations›

definition combinedPairlist_Sync ::
  ‹[('σ, 'e, 'r, 'α) Ad_scheme, 'e set, ('σ, 'e, 'r, 'β) Ad_scheme] ⇒ ('σ list, 'e, 'r) Ad›
  where ‹combinedPairlist_Sync A0 E A1 ≡
         combined_Sync A0 E A1 hd (λσs. hd (tl σs)) (λs t. [s, t]) (λs t. if s = t then ⌊s⌋ else ◇)›
definition combinendPairlist_Sync ::
  ‹[('σ, 'e, 'r, 'α) And_scheme, 'e set, ('σ, 'e, 'r, 'β) And_scheme] ⇒ ('σ list, 'e, 'r) And›
  where ‹combinendPairlist_Sync A0 E A1 ≡
         combinend_Sync A0 E A1 hd (λσs. hd (tl σs)) (λs t. [s, t]) (λs t. if s = t then ⌊s⌋ else ◇)›

definition combinedPair_Sync ::
  ‹[('σ0, 'e, 'r, 'α) Ad_scheme, 'e set, ('σ1, 'e, 'r, 'β) Ad_scheme] ⇒ ('σ0 × 'σ1, 'e, 'r) Ad›
  where ‹combinedPair_Sync A0 E A1 ≡
         combined_Sync A0 E A1 fst snd Pair (λs t. if s = t then ⌊s⌋ else ◇)›
definition combinendPair_Sync ::
  ‹[('σ0, 'e, 'r, 'α) And_scheme, 'e set, ('σ1, 'e, 'r, 'β) And_scheme] ⇒ ('σ0 × 'σ1, 'e, 'r) And›
  where ‹combinendPair_Sync A0 E A1 ≡
         combinend_Sync A0 E A1 fst snd Pair (λs t. if s = t then ⌊s⌋ else ◇)›

definition combinedListslenL_Sync ::
  ‹[('σ list, 'e, 'r, 'α) Ad_scheme, nat, 'e set, ('σ list, 'e, 'r, 'β) Ad_scheme] ⇒ ('σ list, 'e, 'r) Ad›
  where ‹combinedListslenL_Sync A0 len0 E A1 ≡
         combined_Sync A0 E A1 (take len0) (drop len0) (@) (λs t. if s = t then ⌊s⌋ else ◇)›
definition combinendListslenL_Sync ::
  ‹[('σ list, 'e, 'r, 'α) And_scheme, nat, 'e set, ('σ list, 'e, 'r, 'β) And_scheme] ⇒ ('σ list, 'e, 'r) And›
  where ‹combinendListslenL_Sync A0 len0 E A1 ≡
         combinend_Sync A0 E A1 (take len0) (drop len0) (@) (λs t. if s = t then ⌊s⌋ else ◇)›

definition combinedRlist_Sync ::
  ‹[('σ, 'e, 'r, 'α) Ad_scheme, 'e set, ('σ list, 'e, 'r, 'β) Ad_scheme]  ⇒ ('σ list, 'e, 'r) Ad›
  where ‹combinedRlist_Sync A0 E A1 ≡
         combined_Sync A0 E A1 hd tl (#) (λs t. if s = t then ⌊s⌋ else ◇)›
definition combinendRlist_Sync ::
  ‹[('σ, 'e, 'r, 'α) And_scheme, 'e set, ('σ list, 'e, 'r, 'β) And_scheme]  ⇒ ('σ list, 'e, 'r) And›
  where ‹combinendRlist_Sync A0 E A1 ≡
         combinend_Sync A0 E A1 hd tl (#) (λs t. if s = t then ⌊s⌋ else ◇)›

lemmas combinePairlist_Sync_defs = combinedPairlist_Sync_def combinendPairlist_Sync_def
  and combinePair_Sync_defs = combinedPair_Sync_def combinendPair_Sync_def
  and combineListslenL_Sync_defs = combinedListslenL_Sync_def combinendListslenL_Sync_def
  and combineRlist_Sync_defs = combinedRlist_Sync_def combinendRlist_Sync_def

lemmas combine_Sync_defs =
  combinePairlist_Sync_defs combinePair_Sync_defs combineListslenL_Sync_defs combineRlist_Sync_defs


bundle combinend_Sync_syntax begin

notation combinedPairlist_Sync (‹⟪_ d⊗⟦_⟧Pairlist _⟫› [0, 0, 0])
notation combinendPairlist_Sync (‹⟪_ nd⊗⟦_⟧Pairlist _⟫› [0, 0, 0])
notation combinedPair_Sync (‹⟪_ d⊗⟦_⟧Pair _⟫› [0, 0, 0])
notation combinendPair_Sync (‹⟪_ nd⊗⟦_⟧Pair _⟫› [0, 0, 0])
notation combinedListslenL_Sync (‹⟪_ d⊗⟦_, _⟧ListslenL _⟫› [0, 0, 0, 0])
notation combinendListslenL_Sync (‹⟪_ nd⊗⟦_, _⟧ListslenL _⟫› [0, 0, 0, 0])
notation combinedRlist_Sync (‹⟪_ d⊗⟦_⟧Rlist _⟫› [0, 0, 0])
notation combinendRlist_Sync (‹⟪_ nd⊗⟦_⟧Rlist _⟫› [0, 0, 0])

end

unbundle combinend_Sync_syntax



section ‹First Properties›

lemma finite_trans_combinend_Sync_simps [simp] : 
  ‹finite_trans A0 ⟹ finite_trans A1 ⟹ finite_trans ⟪A0 nd⊗⟦E⟧Pairlist A1⟫›
  ‹finite_trans B0 ⟹ finite_trans B1 ⟹ finite_trans ⟪B0 nd⊗⟦E⟧Pair B1⟫›
  ‹finite_trans C0 ⟹ finite_trans C1 ⟹ finite_trans ⟪C0 nd⊗⟦len0, E⟧ListslenL C1⟫›
  ‹finite_trans D0 ⟹ finite_trans D1 ⟹ finite_trans ⟪D0 nd⊗⟦E⟧Rlist D1⟫›
  unfolding combinendPairlist_Sync_def combinendPair_Sync_def combinendListslenL_Sync_def combinendRlist_Sync_def 
  by (simp_all add: finite_trans_def finite_image_set2)

lemma ε_combinePairlist_Sync:
  ‹ε ⟪A0 d⊗⟦E⟧Pairlist A1⟫ σs = combine_Sync_ε A0 E A1 hd (hd ∘ tl) σs›
  ‹ε ⟪B0 nd⊗⟦E⟧Pairlist B1⟫ σs = combine_Sync_ε B0 E B1 hd (hd ∘ tl) σs›
  by (auto simp add: combine_Sync_ε_def_bis combinePairlist_Sync_defs ε_simps)

lemma ε_combinePair_Sync:
  ‹ε ⟪A0 d⊗⟦E⟧Pair A1⟫ σs = combine_Sync_ε A0 E A1 fst snd σs›
  ‹ε ⟪B0 nd⊗⟦E⟧Pair B1⟫ σs = combine_Sync_ε B0 E B1 fst snd σs›
  by (auto simp add: combine_Sync_ε_def_bis combinePair_Sync_defs ε_simps)

lemma ε_combineListslenL_Sync: 
  ‹ε ⟪A0 d⊗⟦len0, E⟧ListslenL A1⟫ σs = combine_Sync_ε A0 E A1 (take len0) (drop len0) σs›
  ‹ε ⟪B0 nd⊗⟦len0, E⟧ListslenL B1⟫ σs = combine_Sync_ε B0 E B1 (take len0) (drop len0) σs›
  by (auto simp add: combine_Sync_ε_def_bis combineListslenL_Sync_defs ε_simps)

lemma ε_combineRlist_Sync:
  ‹ε ⟪A0 d⊗⟦E⟧Rlist A1⟫ σs = combine_Sync_ε A0 E A1 hd tl σs›
  ‹ε ⟪B0 nd⊗⟦E⟧Rlist B1⟫ σs = combine_Sync_ε B0 E B1 hd tl σs›
  by (auto simp add: combine_Sync_ε_def_bis combineRlist_Sync_defs ε_simps)


lemma ρ_combinePairlist_Sync:
  ‹ρ ⟪A0 d⊗⟦E⟧Pairlist A1⟫ = {σs. hd σs ∈ ρ A0 ∧ hd (tl σs) ∈ ρ A1 ∧ ω A0 (hd σs) = ω A1 (hd (tl σs))}›
  ‹ρ ⟪B0 nd⊗⟦E⟧Pairlist B1⟫ = {σs. hd σs ∈ ρ B0 ∧ hd (tl σs) ∈ ρ B1 ∧ ω B0 (hd σs) ∩ ω B1 (hd (tl σs)) ≠ {}}›
  by (auto simp add: combinePairlist_Sync_defs ρ_simps split: option.split)

lemma ρ_combinePair_Sync:
  ‹ρ ⟪A0 d⊗⟦E⟧Pair A1⟫ = {(σ0, σ1). σ0 ∈ ρ A0 ∧ σ1 ∈ ρ A1 ∧ ω A0 σ0 = ω A1 σ1}›
  ‹ρ ⟪B0 nd⊗⟦E⟧Pair B1⟫ = {(σ0, σ1). σ0 ∈ ρ B0 ∧ σ1 ∈ ρ B1 ∧ ω B0 σ0 ∩ ω B1 σ1 ≠ {}}›
  by (auto simp add: combinePair_Sync_defs ρ_simps split: option.split)

lemma ρ_combineListslenL_Sync: 
  ‹ρ ⟪A0 d⊗⟦len0, E⟧ListslenL A1⟫ =
   {σs. take len0 σs ∈ ρ A0 ∧ drop len0 σs ∈ ρ A1 ∧ ω A0 (take len0 σs) = ω A1 (drop len0 σs)}›
  ‹ρ ⟪B0 nd⊗⟦len0, E⟧ListslenL B1⟫ =
   {σs. take len0 σs ∈ ρ B0 ∧ drop len0 σs ∈ ρ B1 ∧ ω B0 (take len0 σs) ∩ ω B1 (drop len0 σs) ≠ {}}›
  by (auto simp add: combineListslenL_Sync_defs ρ_simps split: option.split)

lemma ρ_combineRlist_Sync:
  ‹ρ ⟪A0 d⊗⟦E⟧Rlist A1⟫ =
   {σs. hd σs ∈ ρ A0 ∧ tl σs ∈ ρ A1 ∧ ω A0 (hd σs) = ω A1 (tl σs)}›
  ‹ρ ⟪B0 nd⊗⟦E⟧Rlist B1⟫ =
   {σs. hd σs ∈ ρ B0 ∧ tl σs ∈ ρ B1 ∧ ω B0 (hd σs) ∩ ω B1 (tl σs) ≠ {}}›
  by (auto simp add: combineRlist_Sync_defs ρ_simps split: option.split)



lemma combine_Sync_τ [simp] :
  ‹combined_Sync_τ (A0⦇ω := some_ω0⦈) E (A1⦇ω := some_ω1⦈) = combined_Sync_τ A0 E A1›
  ‹combinend_Sync_τ (B0⦇ω := some_ω0'⦈) E (B1⦇ω := some_ω1'⦈) = combinend_Sync_τ B0 E B1›
  for A :: ‹('σ, 'a, 'σ option, 'r option, 'α) A_scheme›
    and B :: ‹('σ, 'a, 'σ set, 'r set, 'α) A_scheme›
  by (intro ext, simp)+





section ‹Reachability›

lemma ℛd_combinedListslenL_Sync_subset: 
  ‹ℛd ⟪A0 d⊗⟦len0, E⟧ListslenL A1⟫ (s0 @ s1) ⊆ {t0 @ t1| t0 t1. t0 ∈ ℛd A0 s0 ∧ t1 ∈ ℛd A1 s1}› (is ‹?SA ⊆ _›)
  if same_length_ℛd: ‹⋀t0. t0 ∈ ℛd A0 s0 ⟹ length t0 = len0›
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = t0 @ t1 ∧ t0 ∈ ℛd A0 s0 ∧ t1 ∈ ℛd A1 s1› for t
    apply (induct rule: ℛd.induct, metis ℛd.init)
    by (simp_all add: combineListslenL_Sync_defs same_length_ℛd ε_simps split: if_splits)
      (metis (no_types, opaque_lifting) ℛd.simps)+
qed

lemma ℛnd_combinendListslenL_Sync_subset: 
  ‹ℛnd ⟪B0 nd⊗⟦len0, E⟧ListslenL B1⟫ (s0 @ s1) ⊆ {t0 @ t1| t0 t1. t0 ∈ ℛnd B0 s0 ∧ t1 ∈ ℛnd B1 s1}› (is ‹?SB ⊆ _›)
  if same_length_ℛnd: ‹⋀t0. t0 ∈ ℛnd B0 s0 ⟹ length t0 = len0›
proof safe
  show ‹t ∈ ?SB ⟹ ∃t0 t1. t = t0 @ t1 ∧ t0 ∈ ℛnd B0 s0 ∧ t1 ∈ ℛnd B1 s1› for t
    apply (induct rule: ℛnd.induct, metis ℛnd.init)
    by (simp_all add: combineListslenL_Sync_defs same_length_ℛnd ε_simps split: if_splits)
      (metis (no_types, opaque_lifting) ℛnd.simps)+
qed


lemma ℛd_combinedPairlist_Sync_subset:
  ‹ℛd ⟪A0 d⊗⟦E⟧Pairlist A1⟫ [s0, s1] ⊆ {[t0, t1]| t0 t1. t0 ∈ ℛd A0 s0 ∧ t1 ∈ ℛd A1 s1}› (is ‹?SA ⊆ _›)
  and ℛnd_combinendPairlist_Sync_subset:
  ‹ℛnd ⟪B0 nd⊗⟦E⟧Pairlist B1⟫ [s0, s1] ⊆ {[t0, t1]| t0 t1. t0 ∈ ℛnd B0 s0 ∧ t1 ∈ ℛnd B1 s1}› (is ‹?SB ⊆ _›)
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 t1. t = [t0, t1] ∧ t0 ∈ ℛd A0 s0 ∧ t1 ∈ ℛd A1 s1› for t
    by (ℛd_subset_method defs: combinePairlist_Sync_defs)
  show ‹t ∈ ?SB ⟹ ∃t0 t1. t = [t0, t1] ∧ t0 ∈ ℛnd B0 s0 ∧ t1 ∈ ℛnd B1 s1› for t
    by (ℛnd_subset_method defs: combinePairlist_Sync_defs)
qed

lemma ℛd_combinedPair_Sync_subset:
  ‹ℛd ⟪A0 d⊗⟦E⟧Pair A1⟫ (s0, s1) ⊆ ℛd A0 s0 × ℛd A1 s1› (is ‹?SA ⊆ _›)
  and ℛnd_combinendPair_Sync_subset:
  ‹ℛnd ⟪B0 nd⊗⟦E⟧Pair B1⟫ (s0, s1) ⊆ ℛnd B0 s0 × ℛnd B1 s1› (is ‹?SB ⊆ _›)
proof -
  have ‹t ∈ ?SA ⟹ fst t ∈ ℛd A0 s0 ∧ snd t ∈ ℛd A1 s1› for t 
    by (ℛd_subset_method defs: combinePair_Sync_defs)
  thus ‹?SA ⊆ ℛd A0 s0 × ℛd A1 s1› by force
next
  have ‹t ∈ ?SB ⟹ fst t ∈ ℛnd B0 s0 ∧ snd t ∈ ℛnd B1 s1› for t
    by (ℛnd_subset_method defs: combinePair_Sync_defs)
  thus ‹?SB ⊆ ℛnd B0 s0 × ℛnd B1 s1› by force
qed


lemma ℛd_combinedRlist_Sync_subset:
  ‹ℛd ⟪A0 d⊗⟦E⟧Rlist A1⟫ (s0 # σs) ⊆ {t0 # σt| t0 σt. t0 ∈ ℛd A0 s0 ∧ σt ∈ ℛd A1 σs}› (is ‹?SA ⊆ _›)
  and ℛnd_combinendRlist_Sync_subset: 
  ‹ℛnd ⟪B0 nd⊗⟦E⟧Rlist B1⟫ (s0 # σs) ⊆ {t0 # σt| t0 σt. t0 ∈ ℛnd B0 s0 ∧ σt ∈ ℛnd B1 σs}› (is ‹?SB ⊆ _›)
proof safe
  show ‹t ∈ ?SA ⟹ ∃t0 σt. t = t0 # σt ∧ t0 ∈ ℛd A0 s0 ∧ σt ∈ ℛd A1 σs› for t
    by (ℛd_subset_method defs: combineRlist_Sync_defs)
next
  show ‹t ∈ ?SB ⟹ ∃t0 σt. t = t0 # σt ∧ t0 ∈ ℛnd B0 s0 ∧ σt ∈ ℛnd B1 σs› for t
    by (ℛnd_subset_method defs: combineRlist_Sync_defs)
qed



section ‹Normalization› 


lemma ω_combinePairlist_Sync_behaviour:
  ‹ω ⟪⟪A0 d⊗⟦E⟧Pairlist A1⟫⟫d↪nd [s0, s1] = ω ⟪⟪A0⟫d↪nd nd⊗⟦E⟧Pairlist ⟪A1⟫d↪nd⟫ [s0, s1]›
  by (auto simp add: combinePairlist_Sync_defs det_ndet_conv_defs option.case_eq_if)

lemma ω_combinePair_Sync_behaviour:
  ‹ω ⟪⟪A0 d⊗⟦E⟧Pair A1⟫⟫d↪nd (s0, s1) = ω ⟪⟪A0⟫d↪nd nd⊗⟦E⟧Pair ⟪A1⟫d↪nd⟫ (s0, s1)›
  by (auto simp add: combinePair_Sync_defs det_ndet_conv_defs option.case_eq_if)

lemma ω_combineListslenL_Sync_behaviour:
  ‹ω ⟪⟪A0 d⊗⟦len0, E⟧ListslenL A1⟫⟫d↪nd (σs0 @ σs1) = ω ⟪⟪A0⟫d↪nd nd⊗⟦len0, E⟧ListslenL ⟪A1⟫d↪nd⟫ (σs0 @ σs1)›
  by (auto simp add: combineListslenL_Sync_defs det_ndet_conv_defs option.case_eq_if)

lemma ω_combineRlist_Sync_behaviour:
  ‹ω ⟪⟪A0 d⊗⟦E⟧Rlist A1⟫⟫d↪nd (s0 # σs1) = ω ⟪⟪A0⟫d↪nd nd⊗⟦E⟧Rlist ⟪A1⟫d↪nd⟫ (s0 # σs1)›
  by (auto simp add: combineRlist_Sync_defs det_ndet_conv_defs option.case_eq_if)


lemma τ_combinePairlist_Sync_behaviour_when_indep:
  ‹ε A0 s0 ∩ ε A1 s1 ⊆ E ⟹
   τ ⟪⟪A0 d⊗⟦E⟧Pairlist A1⟫⟫d↪nd [s0, s1] e = τ ⟪⟪A0⟫d↪nd nd⊗⟦E⟧Pairlist ⟪A1⟫d↪nd⟫ [s0, s1] e›
  by (auto simp add: combinePairlist_Sync_defs det_ndet_conv_defs option.case_eq_if ε_simps)

lemma τ_combinePair_Sync_behaviour_when_indep:
  ‹ε A0 s0 ∩ ε A1 s1 ⊆ E ⟹ 
   τ ⟪⟪A0 d⊗⟦E⟧Pair A1⟫⟫d↪nd (s0, s1) e = τ ⟪⟪A0⟫d↪nd nd⊗⟦E⟧Pair ⟪A1⟫d↪nd⟫ (s0, s1) e›
  by (auto simp add: combinePair_Sync_defs det_ndet_conv_defs option.case_eq_if ε_simps)

lemma τ_combineListslenL_Sync_behaviour_when_indep:
  ‹ε A0 σs0 ∩ ε A1 σs1 ⊆ E ⟹ length σs0 = len0 ⟹ 
   τ ⟪⟪A0 d⊗⟦len0, E⟧ListslenL A1⟫⟫d↪nd (σs0 @ σs1) e = τ ⟪⟪A0⟫d↪nd nd⊗⟦len0, E⟧ListslenL ⟪A1⟫d↪nd⟫ (σs0 @ σs1) e›
  by (auto simp add: combineListslenL_Sync_defs det_ndet_conv_defs option.case_eq_if ε_simps)

lemma τ_combineRlist_Sync_behaviour_when_indep:
  ‹ε A0 s0 ∩ ε A1 σs1 ⊆ E ⟹
   τ ⟪⟪A0 d⊗⟦E⟧Rlist A1⟫⟫d↪nd (s0 # σs1) e = τ ⟪⟪A0⟫d↪nd nd⊗⟦E⟧Rlist ⟪A1⟫d↪nd⟫ (s0 # σs1) e›
  by (auto simp add: combineRlist_Sync_defs det_ndet_conv_defs option.case_eq_if ε_simps)



method PSKIPS_when_indep_method uses R_d_subset = 
  fold PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d,
  rule PSKIPS_nd_eqI_strong_id,
  unfold ℛnd_from_det_to_ndet,
  all ‹drule set_mp[OF R_d_subset, rotated]›


method P_when_indep_method uses R_d_subset =
  fold P_nd_from_det_to_ndet_is_P_d,
  rule P_nd_eqI_strong_id,
  unfold ℛnd_from_det_to_ndet,
  all ‹drule set_mp[OF R_d_subset, rotated]›


lemma PSKIPS_combinePairlist_Sync_behaviour_when_indep:
  ‹PSKIPS⟪⟪A0 d⊗⟦E⟧Pairlist A1⟫⟫d [s0, s1] = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧Pairlist ⟪A1⟫d↪nd⟫⟫nd [s0, s1]›
  if ‹indep_enabl A0 s0 E A1 s1›
  by (PSKIPS_when_indep_method R_d_subset: ℛd_combinedPairlist_Sync_subset, simp_all)
    (metis τ_combinePairlist_Sync_behaviour_when_indep indep_enablD that,
      metis ω_combinePairlist_Sync_behaviour)

lemma P_combinePairlist_Sync_behaviour_when_indep:
  ‹P⟪⟪A0 d⊗⟦E⟧Pairlist A1⟫⟫d [s0, s1] = P⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧Pairlist ⟪A1⟫d↪nd⟫⟫nd [s0, s1]›
  if ‹indep_enabl A0 s0 E A1 s1›
  by (P_when_indep_method R_d_subset: ℛd_combinedPairlist_Sync_subset, simp_all)
    (metis τ_combinePairlist_Sync_behaviour_when_indep indep_enablD that)


lemma PSKIPS_combinePair_Sync_behaviour_when_indep:
  ‹PSKIPS⟪⟪A0 d⊗⟦E⟧Pair A1⟫⟫d (s0, s1) = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧Pair ⟪A1⟫d↪nd⟫⟫nd (s0, s1)›
  if ‹indep_enabl A0 s0 E A1 s1›
  by (PSKIPS_when_indep_method R_d_subset: ℛd_combinedPair_Sync_subset, all ‹elim SigmaE›)
    (metis τ_combinePair_Sync_behaviour_when_indep indep_enablD that,
      auto simp add: ω_combinePair_Sync_behaviour option.case_eq_if)

lemma P_combinePair_Sync_behaviour_when_indep:
  ‹P⟪⟪A0 d⊗⟦E⟧Pair A1⟫⟫d (s0, s1) = P⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧Pair ⟪A1⟫d↪nd⟫⟫nd (s0, s1)›
  if ‹indep_enabl A0 s0 E A1 s1›
  by (P_when_indep_method R_d_subset: ℛd_combinedPair_Sync_subset, elim SigmaE)
    (metis τ_combinePair_Sync_behaviour_when_indep indep_enablD that)


lemma PSKIPS_combineListslenL_Sync_behaviour_when_indep:
  ‹PSKIPS⟪⟪A0 d⊗⟦len0, E⟧ListslenL A1⟫⟫d (σs0 @ σs1) = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦len0, E⟧ListslenL ⟪A1⟫d↪nd⟫⟫nd (σs0 @ σs1)› 
  if ‹indep_enabl A0 σs0 E A1 σs1› and ‹⋀σt0. σt0 ∈ ℛd A0 σs0 ⟹ length σt0 = len0›
  by (PSKIPS_when_indep_method R_d_subset: ℛd_combinedListslenL_Sync_subset, simp_all add: that(2))
    (metis τ_combineListslenL_Sync_behaviour_when_indep indep_enablD that,
      metis ω_combineListslenL_Sync_behaviour)

lemma P_combineListslenL_Sync_behaviour_when_indep:
  ‹P⟪⟪A0 d⊗⟦len0, E⟧ListslenL A1⟫⟫d (σs0 @ σs1) = P⟪⟪⟪A0⟫d↪nd nd⊗⟦len0, E⟧ListslenL ⟪A1⟫d↪nd⟫⟫nd (σs0 @ σs1)›
  if ‹indep_enabl A0 σs0 E A1 σs1› and ‹⋀σt0. σt0 ∈ ℛd A0 σs0 ⟹ length σt0 = len0›
  by (P_when_indep_method R_d_subset: ℛd_combinedListslenL_Sync_subset, simp_all add: that(2))
    (metis τ_combineListslenL_Sync_behaviour_when_indep indep_enablD that)


lemma PSKIPS_combineRlist_Sync_behaviour_when_indep:
  ‹PSKIPS⟪⟪A0 d⊗⟦E⟧Rlist A1⟫⟫d (s0 # σs1) = PSKIPS⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧Rlist ⟪A1⟫d↪nd⟫⟫nd (s0 # σs1)›
  if ‹indep_enabl A0 s0 E A1 σs1›
  by (PSKIPS_when_indep_method R_d_subset: ℛd_combinedRlist_Sync_subset, simp_all)
    (metis τ_combineRlist_Sync_behaviour_when_indep indep_enablD that,
      metis ω_combineRlist_Sync_behaviour)

lemma P_combineRlist_Sync_behaviour_when_indep:
  ‹P⟪⟪A0 d⊗⟦E⟧Rlist A1⟫⟫d (s0 # σs1) = P⟪⟪⟪A0⟫d↪nd nd⊗⟦E⟧Rlist ⟪A1⟫d↪nd⟫⟫nd (s0 # σs1)›
  if ‹indep_enabl A0 s0 E A1 σs1›
  by (P_when_indep_method R_d_subset: ℛd_combinedRlist_Sync_subset, simp)
    (metis τ_combineRlist_Sync_behaviour_when_indep indep_enablD that)


(*<*)
end
  (*>*)