Theory Multi_Sequential_Composition_Generalized

(***********************************************************************************
 * 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 ‹Architectural Versions›

section ‹Sequential Composition›

(*<*)
theory Multi_Sequential_Composition_Generalized
  imports Synchronization_Product_Generalized_Interpretations
begin
  (*>*)


subsection ‹Definition›

fun MultiSeqptick :: ‹['b list, 'b ⇒ 'r ⇒ ('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
  where MultiSeqptick_Nil  : ‹MultiSeqptick   []    P = SKIP›
  |     MultiSeqptick_Cons : ‹MultiSeqptick (l # L) P = (λr. P l r ;✓ MultiSeqptick L P)›


syntax  "_MultiSeqptick" ::
  ‹[pttrn, 'b list, 'b ⇒ 'r ⇒ ('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
  (‹(3SEQ✓ _ ∈@ _./ _)› [78,78,77] 77)
syntax_consts "_MultiSeqptick" ⇌ MultiSeqptick
translations  "SEQ✓ p ∈@ L. P" ⇌ "CONST MultiSeqptick L (λp. P)"



subsection ‹First Properties›

―‹Some tests›
lemma ‹SEQ✓ p ∈@ []. P p = SKIP› 
  and ‹SEQ✓ p ∈@ [a]. P p = (λr. P a r)› 
  and ‹SEQ✓ p ∈@ [a, b]. P p = (λr. P a r ;✓ P b)› 
  and ‹SEQ✓ p ∈@ [a, b, c]. P p = (λr. P a r ;✓ P b ;✓ P c)› 
  by (simp_all add: Seqptick_assoc)

lemma ‹SEQ✓ p ∈@ [1::int .. 3]. P p = (λr. P 1 r ;✓ P 2 ;✓ P 3)›
  by (simp add: upto.simps Seqptick_assoc)



lemma ‹(SEQ✓ p ∈@ []. P p) = SKIP› by (fact MultiSeqptick_Nil)

lemma ‹(SEQ✓ l ∈@ (a # L). P l) = (λr. P a r ;✓ SEQ✓ l ∈@ L. P l)› by (fact MultiSeqptick_Cons)


lemma MultiSeqptick_singl [simp] : ‹SEQ✓ l ∈@ [a]. P l = P a› by simp

lemma MultiSeqptick_snoc : ‹SEQ✓ l ∈@ (L @ [a]). P l = (λr. (SEQ✓ l ∈@ L. P l) r ;✓ P a)›
  by (induct L) (simp_all add: Seqptick_assoc)


lemma mono_MultiSeqptick_eq:
  ‹(⋀l. l ∈ set L ⟹ P l = Q l) ⟹ SEQ✓ l ∈@ L. P l = SEQ✓ l ∈@ L. Q l›
  by (induct L) fastforce+


lemma MultiSeqptick_const [simp] :
  ‹(SEQ✓ l ∈@ L. (λr. P l)) =
   (if L = [] then SKIP else (λr. SEQ l ∈@ L. P l))›
  by (induct L rule: rev_induct) (auto simp add: MultiSeqptick_snoc)



subsection ‹Behaviour with binary version›

lemma MultiSeqptick_append:
  ‹SEQ✓ l ∈@ (L1 @ L2). P l = (λr. (SEQ✓ l ∈@ L1. P l) r ;✓ SEQ✓ l ∈@ L2. P l)›
  by (induct L1 rule: list.induct, simp_all, metis Seqptick_assoc)



subsection ‹Other Properties›

lemma MultiSeqptick_SKIP_neutral:
  ‹P a = SKIP ⟹ SEQ✓ l ∈@ (L1 @ [a] @ L2). P l = SEQ✓ l ∈@ (L1 @ L2). P l›
  by (simp add: MultiSeqptick_append)

lemma MultiSeqptick_BOT_absorb:
  ‹P a = ⊥ ⟹ SEQ✓ l ∈@ (L1 @ [a] @ L2). P l = (λr. (SEQ✓ l ∈@ L1. P l) r ;✓ ⊥)›
  by (simp add: MultiSeqptick_append lambda_strict)

lemma MultiSeqptick_STOP_absorb:
  ‹P a = (λr. STOP) ⟹ SEQ✓ l ∈@ (L1 @ [a] @ L2). P l =
                        (λr. (SEQ✓ l ∈@ L1. P l) r ; STOP)›
  by (simp add: MultiSeqptick_append)

lemma is_ticks_length_MultiSeqptick [is_ticks_length_intro] :
  ‹length✓⇘n⇙((SEQ✓ l ∈@ L. P l) r)›
  if ‹L ≠ []› and ‹⋀r'. r' ∈ ✓s((SEQ✓ l ∈@ (butlast L). P l) r) ⟹ length✓⇘n⇙(P (last L) r')›
proof -
  from that(1) obtain l L' where ‹L = L' @ [l]›
    by (cases L rule: rev_cases) auto
  with that(2) have ‹r' ∈ ✓s((SEQ✓ l ∈@ L'. P l) r) ⟹ length✓⇘n⇙(P l r')› for r' by simp
  thus ?thesis
    by (auto simp add: ‹L = L' @ [l]› MultiSeqptick_snoc intro: is_ticks_length_Seqptick)
qed


subsection ‹Behaviour with injectivity›

lemma inj_on_mapping_over_MultiSeqptick:
  ‹inj_on f (set L) ⟹
   SEQ✓ l ∈@ L. P l = SEQ✓ l ∈@ map f L. P (inv_into (set L) f l)›
proof (induct L)
  show ‹inj_on f (set []) ⟹ MultiSeqptick [] P =
        SEQ✓ x∈@map f []. P (inv_into (set []) f x)› by simp
next
  case (Cons a L)
  show ?case
  proof (rule ext)
    fix r
    have ‹(SEQ✓ l ∈@ (a # L). P l) r = P a r ;✓ SEQ✓ l ∈@ L. P l› by simp
    also have ‹SEQ✓ l ∈@ L. P l = SEQ✓ l ∈@ map f L. P (inv_into (set L) f l)›
      using Cons.hyps Cons.prems by auto
    also have ‹… = SEQ✓ l ∈@ map f L. P (inv_into (set (a # L)) f l)›
      using Cons.prems by (auto intro!: mono_MultiSeqptick_eq)
    finally show ‹(SEQ✓ l ∈@ (a # L). P l) r =
                  (SEQ✓ l ∈@ map f (a # L). P (inv_into (set (a # L)) f l)) r›
      using Cons.prems by auto
  qed
qed



(*<*)
end
  (*>*)