Theory Multi_Sequential_Composition

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : Multi sequential composition
 *
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * 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 list of conditions and the following disclaimer.
 *
 *     * 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.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * 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
 * OWNER 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.
 ******************************************************************************›
(*>*)


section ‹Multiple Sequential Composition›

(*<*)
theory Multi_Sequential_Composition
  imports "HOL-CSP.CSP"
begin
  (*>*)

text ‹Because of the fact that termSKIP r is not exactly a neutral element for
      @{const [source] Seq} (cf @{thm SKIP_Seq Seq_SKIP}), we do the folding
      on the reversed list.›


subsection ‹Definition›

fun MultiSeq_rev :: ['b list, 'b  ('a, 'r) processptick]  ('a, 'r) processptick
  where MultiSeq_rev_Nil  : MultiSeq_rev   []    P = SKIP undefined
  |     MultiSeq_rev_Cons : MultiSeq_rev (l # L) P = MultiSeq_rev L P ; P l


definition MultiSeq :: ['b list, 'b  ('a, 'r) processptick]  ('a, 'r) processptick
  where MultiSeq L P  MultiSeq_rev (rev L) P


lemma MultiSeq_Nil  [simp] : MultiSeq []        P = SKIP undefined
  and MultiSeq_snoc [simp] : MultiSeq (L @ [l]) P = MultiSeq L P ; P l
  by (simp_all add: MultiSeq_def)


lemma MultiSeq_elims :
  MultiSeq L P = Q 
   (P'. L = []  P = P'  Q = SKIP undefined  thesis) 
   (l L' P'. L = L' @ [l]  P = P'  Q = MultiSeq L' P' ; P' l  thesis)  thesis
  by (simp add: MultiSeq_def, erule MultiSeq_rev.elims, simp_all)



syntax  "_MultiSeq" :: [pttrn, 'b list, 'b  'r  ('a, 'r) processptick, 'r]  ('a, 'r) processptick
  ((3SEQ _∈@_./ _) [78,78,77] 77)
syntax_consts "_MultiSeq"  MultiSeq
translations  "SEQ p ∈@ L. P"  "CONST MultiSeq L (λp. P)"



subsection ‹First Properties›

lemma SEQ p ∈@ []. P p = SKIP undefined by (fact MultiSeq_Nil)

lemma SEQ i ∈@ (L @ [l]). P i = SEQ i ∈@ L. P i ; P l by (fact MultiSeq_snoc)

lemma MultiSeq_singl [simp] : SEQ l ∈@ [l]. P l = P l by (simp add: MultiSeq_def)



subsection ‹Some Tests›

lemma SEQ p ∈@ []. P p = SKIP undefined 
  and SEQ p ∈@ [a]. P p = P a 
  and SEQ p ∈@ [a, b]. P p = P a ; P b 
  and SEQ p ∈@ [a, b, c]. P p = P a ; P b ; P c
  by (simp_all add: MultiSeq_def)


lemma test_MultiSeq: (SEQ p ∈@ [1::int .. 3]. P p) = P 1 ; P 2 ; P 3
  by (simp add: upto.simps MultiSeq_def)


subsection ‹Continuity›

lemma mono_MultiSeq :
  (x. x  set L  P x  Q x)  SEQ l ∈@ L. P l  SEQ l ∈@ L. Q l
  by (induct L rule: rev_induct, simp_all add: fun_belowI mono_Seq)

lemma MultiSeq_cont[simp]:
  (x. x  set L  cont (P x))  cont (λy. SEQ z ∈@ L. P z y)
  by (induct L rule: rev_induct) simp_all



subsection ‹Factorization of constSeq in front of constMultiSeq

lemma MultiSeq_factorization_append:
  L2  []  SEQ p ∈@ L1. P p ; SEQ p ∈@ L2. P p = SEQ p ∈@ (L1 @ L2). P p
  by (induct L2 rule: rev_induct, simp_all)
    (metis (no_types, lifting) MultiSeq_singl MultiSeq_snoc
      Seq_assoc append_assoc append_self_conv2)



subsection term Absorbtion›


lemma MultiSeq_BOT_absorb:
  SEQ z ∈@ (L1 @ a # L2). P z = SEQ z ∈@ L1. P z ;  if P a = 
proof (cases L2 = [])
  from P a =  show L2 = []  MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ;  by simp
next
  show L2  []  MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ; 
    by (simp add: P a =  flip: Seq_assoc MultiSeq_factorization_append
        [of L2 L1 @ [a], simplified])
qed



subsection ‹First Properties›

lemma MultiSeq_SKIP_neutral:
  SEQ z ∈@ (L1 @ a # L2). P z =
   (  if L2 = [] then SEQ z ∈@ L1. P z ; SKIP r
    else SEQ z ∈@ (L1 @ L2). P z) if P a = SKIP r
proof (split if_split, intro conjI impI)
  show L2 = []  MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ; SKIP r
    by (simp add: P a = SKIP r)
next
  assume L2  []
  have MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ; P a ; MultiSeq L2 P
    by (metis (mono_tags, opaque_lifting) Cons_eq_appendI MultiSeq_factorization_append
        MultiSeq_snoc L2  [] append_eq_appendI self_append_conv2)
  also have  = MultiSeq L1 P ; MultiSeq L2 P
    by (simp add: P a = SKIP r flip: Seq_assoc)
  also have  = MultiSeq (L1 @ L2) P
    by (simp add: MultiSeq_factorization_append L2  [])
  finally show MultiSeq (L1 @ a # L2) P = MultiSeq (L1 @ L2) P .
qed


lemma MultiSeq_STOP_absorb:
  SEQ z ∈@ (L1 @ a # L2). P z = SEQ z ∈@ L1. P z ; STOP if P a = STOP
proof (cases L2 = [])
  show L2 = []  MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ; STOP
    by (simp add: P a = STOP)
next
  show L2  []  MultiSeq (L1 @ a # L2) P = MultiSeq L1 P ; STOP
    by (simp add: P a = STOP flip: Seq_assoc MultiSeq_factorization_append
        [of L2 L1 @ [a], simplified])
qed


lemma mono_MultiSeq_eq:
  (x. x  set L  P x = Q x)  MultiSeq L P = MultiSeq L Q
  by (induct L rule: rev_induct) simp_all


(* TODO: try this when we will have Seq_is_SKIP_iff *)
(* lemma MultiSeq_is_SKIP_iff:
  ‹MultiSeq L P = SKIP ⟷ (∀a ∈ set L. P a = SKIP)›
  by (induct L, simp_all add: Seq_is_SKIP_iff) *)



subsection ‹Commutativity›

text ‹Of course, since the sequential composition termP ; Q is not commutative,
      the result here is negative: the order of the elements of list termL
      does matter in @{term [eta_contract = false] SEQ z ∈@ L. P z}.›



subsection ‹Behaviour with Injectivity›

lemma inj_on_mapping_over_MultiSeq:
  inj_on f (set C) 
   SEQ x ∈@ C. P x = SEQ x ∈@ map f C. P (inv_into (set C) f x)
proof (induct C rule: rev_induct)
  show inj_on f (set [])  MultiSeq [] P =
        SEQ x∈@map f []. P (inv_into (set []) f x) by simp
next
  case (snoc a C)
  hence f1: inv_into (insert a (set C)) f (f a) = a by force
  show ?case
    apply (simp add: f1, intro ext arg_cong[where f = λx. x ; P a])
    apply (subst "snoc.hyps"(1), rule inj_on_subset[OF "snoc.prems"],
        simp add: subset_insertI)
    using snoc.prems by (auto intro!: mono_MultiSeq_eq)
qed



subsection ‹Definition of first_elem›

primrec first_elem :: ['a  bool, 'a list]  nat
  where first_elem P [] = 0
  |     first_elem P (x # L) = (if P x then 0 else Suc (first_elem P L))

text constfirst_elem returns the first index termi such that
      termP (L ! i) = True if it exists, termlength L otherwise.

      This will be very useful later.›

value first_elem (λx. 4 < x) [0::nat, 2, 5]
lemma first_elem (λx. 5 < x) [0::nat, 2, 5] = 3 by simp 
lemma P ` set L  {False}  first_elem P L = length L by (induct L; simp)


(*<*)
end
  (*>*)